Theorem isset 2778

Description: Two ways to say " A is a set": A class A is a member of the universal class _V (see df-v 2774) 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 4484. Note the when A is not a set, it is called a proper class. In some theorems, such as uniexg 4486, 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 2201 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 2201	. 2 |- ( A e. _V <-> E. x ( x = A /\ x e. _V ) )
2		vex 2775	. . . 4 |- x e. _V
3	2	biantru 302	. . 3 |- ( x = A <-> ( x = A /\ x e. _V ) )
4	3	exbii 1628	. 2 |- ( E. x x = A <-> E. x ( x = A /\ x e. _V ) )
5	1, 4	bitr4i 187	1 |- ( A e. _V <-> E. x x = A )

Syntax hints:   /\ wa 104   <-> wb 105   = wceq 1373   E.wex 1515   e. wcel 2176   _Vcvv 2772

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-v 2774

This theorem is referenced by:  issetf  2779  isseti  2780  issetri  2781  elex  2783  elisset  2786  vtoclg1f  2832  ceqex  2900  eueq  2944  moeq  2948  mosubt  2950  ru  2997  sbc5  3022  snprc  3698  snssb  3766  vprc  4176  opelopabsb  4306  eusvnfb  4501  elrelimasn  5048  euiotaex  5248  fvmptdf  5667  fvmptdv2  5669  fmptco  5746  brabvv  5991  ovmpodf  6077  ovi3  6083  tfrlemibxssdm  6413  tfr1onlembxssdm  6429  tfrcllembxssdm  6442  ecexr  6625  snexxph  7052  fnpr2ob  13172  bj-vprc  15832  bj-vnex  15834  bj-2inf  15874