Description: Two ways to say " A is a set": A class A is a member of the
universal class _V (see df-v ) if and only if the class A
exists (i.e. there exists some set x equal to class A ).
Theorem 6.9 of Quine p. 43.Notational convention: We will use the
notational device " A e.V " to mean " A is a set" very
frequently, for example in uniex . Note that a class A which is
not a set is called a proper class_. In some theorems, such as
uniexg , in order to shorten certain proofs we use the more general
antecedent A e. V instead of A e.V to mean " A is a set."

Note that a constant is implicitly considered distinct from all
variables. This is why V is not included in the distinct variable
list, even though df-clel requires that the expression substituted for
B not contain x . (Also, the Metamath spec does not allow
constants in the distinct variable list.) (Contributed by NM, 26-May-1993)