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 value is a member of without any assumptions. In "negative position", it's a question of whether to spend one extra elex step in some cases (e.g. 2 e. RR therefore 2 e. _V therefore I can apply this lemma about sets to 2), or one extra syntax step to instantiate the V argument (which also takes some space in proofs). I believe the above convention is derived from some analysis along these lines, but it's also somewhat historical (it's more important to have a consistent convention). See the "Is-a-set." section of https://us.metamath.org/mpeuni/conventions.html for more information.
On Wed, Apr 24, 2024 at 3:52 AM heiphohmia via Metamath < [email protected]> wrote: > > 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 <https://us.metamath.org/mpeuni/elex.html> makes it > clear. > > Okay, elements of ZF classes are always sets, so A e. V restricts A from > being > proper classes. That begs the question why one would ever use A e. _V > though. > Is this just a case where there's no particular convention? > > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/272R9VKF3UZLE.34NMDVUCB3A1P%40wilsonb.com > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSsZM-syOfP_R0EaEZrghkTYH1Ci349FFdvUzauXoE7iPg%40mail.gmail.com.
