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 4422. Note the when A is not a set, it is called a proper class. In some theorems, such as uniexg 4424, 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  3648  vprc  4121  opelopabsb  4245  eusvnfb  4439  euiotaex  5176  fvmptdf  5583  fvmptdv2  5585  fmptco  5662  brabvv  5899  ovmpodf  5984  ovi3  5989  tfrlemibxssdm  6306  tfr1onlembxssdm  6322  tfrcllembxssdm  6335  ecexr  6518  snexxph  6927  bj-vprc  13931  bj-vnex  13933  bj-2inf  13973