Theorem isset 2727

Description: Two ways to say " A is a set": A class A is a member of the universal class _V (see df-v 2723) 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 4409. Note the when A is not a set, it is called a proper class. In some theorems, such as uniexg 4411, 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 2160 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 2160	. 2 |- ( A e. _V <-> E. x ( x = A /\ x e. _V ) )
2		vex 2724	. . . 4 |- x e. _V
3	2	biantru 300	. . 3 |- ( x = A <-> ( x = A /\ x e. _V ) )
4	3	exbii 1592	. 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 1342   E.wex 1479   e. wcel 2135   _Vcvv 2721

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 1434  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-v 2723

This theorem is referenced by:  issetf  2728  isseti  2729  issetri  2730  elex  2732  elisset  2735  vtoclg1f  2780  ceqex  2848  eueq  2892  moeq  2896  mosubt  2898  ru  2945  sbc5  2969  snprc  3635  vprc  4108  opelopabsb  4232  eusvnfb  4426  euiotaex  5163  fvmptdf  5567  fvmptdv2  5569  fmptco  5645  brabvv  5879  ovmpodf  5964  ovi3  5969  tfrlemibxssdm  6286  tfr1onlembxssdm  6302  tfrcllembxssdm  6315  ecexr  6497  snexxph  6906  bj-vprc  13613  bj-vnex  13615  bj-2inf  13655