Description: Two ways to say " A is a set": A class A is a member of the universal class _V (see dfv ) 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 dfclel 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, 26May1993)
Ref  Expression  

Assertion  isset   ( A e. _V <> E. x x = A ) 
Step  Hyp  Ref  Expression 

1  dfclel   ( A e. _V <> E. x ( x = A /\ x e. _V ) ) 

2  vex   x e. _V 

3  2  biantru   ( x = A <> ( x = A /\ x e. _V ) ) 
4  3  exbii   ( E. x x = A <> E. x ( x = A /\ x e. _V ) ) 
5  1 4  bitr4i   ( A e. _V <> E. x x = A ) 