Re: [Metamath] Question abouot indistopon

There is a convention, which is to use "( A e. V -> ..." in antecedents to theorems and deduction-form statements and |- A e. _V in inference-form theorems. In "positive position", you often need to use A e. _V, i.e. in fvex there is no other reasonable option for what set to say that function

Re: [Metamath] Question abouot indistopon

> It functions much like A e. _V would. A proof using this theorem can always > plug in _V for V but it also could plug in On, RR, or whatever is convenient. > Perhaps looking at makes it clear. Okay, elements of ZF classes are always sets, so A e. V