Theorem isset 2687

Description: Two ways to say " A is a set": A class A is a member of the universal class _V (see df-v 2683) 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 4354. Note the when A is not a set, it is called a proper class. In some theorems, such as uniexg 4356, 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 2133 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 2133	. 2 |- ( A e. _V <-> E. x ( x = A /\ x e. _V ) )
2		vex 2684	. . . 4 |- x e. _V
3	2	biantru 300	. . 3 |- ( x = A <-> ( x = A /\ x e. _V ) )
4	3	exbii 1584	. 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 1331   E.wex 1468   e. wcel 1480   _Vcvv 2681

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-v 2683

This theorem is referenced by:  issetf  2688  isseti  2689  issetri  2690  elex  2692  elisset  2695  vtoclg1f  2740  ceqex  2807  eueq  2850  moeq  2854  mosubt  2856  ru  2903  sbc5  2927  snprc  3583  vprc  4055  opelopabsb  4177  eusvnfb  4370  euiotaex  5099  fvmptdf  5501  fvmptdv2  5503  fmptco  5579  brabvv  5810  ovmpodf  5895  ovi3  5900  tfrlemibxssdm  6217  tfr1onlembxssdm  6233  tfrcllembxssdm  6246  ecexr  6427  snexxph  6831  bj-vprc  13083  bj-vnex  13085  bj-2inf  13125