Theorem isset 2736

Description: Two ways to say " A is a set": A class A is a member of the universal class _V (see df-v 2732) 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 4420. Note the when A is not a set, it is called a proper class. In some theorems, such as uniexg 4422, 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 2166 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.)

Assertion

Ref	Expression
isset	|- ( A e. _V <-> E. x x = A )

Distinct variable group:   x, A

Proof of Theorem isset

Step	Hyp	Ref	Expression
1		df-clel 2166	. 2 |- ( A e. _V <-> E. x ( x = A /\ x e. _V ) )
2		vex 2733	. . . 4 |- x e. _V
3	2	biantru 300	. . 3 |- ( x = A <-> ( x = A /\ x e. _V ) )
4	3	exbii 1598	. 2 |- ( E. x x = A <-> E. x ( x = A /\ x e. _V ) )
5	1, 4	bitr4i 186	1 |- ( A e. _V <-> E. x x = A )

Syntax hints:   /\ wa 103   <-> wb 104   = wceq 1348   E.wex 1485   e. wcel 2141   _Vcvv 2730

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-v 2732

This theorem is referenced by:  issetf  2737  isseti  2738  issetri  2739  elex  2741  elisset  2744  vtoclg1f  2789  ceqex  2857  eueq  2901  moeq  2905  mosubt  2907  ru  2954  sbc5  2978  snprc  3646  vprc  4119  opelopabsb  4243  eusvnfb  4437  euiotaex  5174  fvmptdf  5581  fvmptdv2  5583  fmptco  5660  brabvv  5897  ovmpodf  5982  ovi3  5987  tfrlemibxssdm  6304  tfr1onlembxssdm  6320  tfrcllembxssdm  6333  ecexr  6516  snexxph  6925  bj-vprc  13896  bj-vnex  13898  bj-2inf  13938