Theorem isset 2647

Description: Two ways to say " A is a set": A class A is a member of the universal class _V (see df-v 2643) 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 4297. Note the when A is not a set, it is called a proper class. In some theorems, such as uniexg 4299, 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 2096 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 2096	. 2 |- ( A e. _V <-> E. x ( x = A /\ x e. _V ) )
2		vex 2644	. . . 4 |- x e. _V
3	2	biantru 298	. . 3 |- ( x = A <-> ( x = A /\ x e. _V ) )
4	3	exbii 1552	. 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 1299   E.wex 1436   e. wcel 1448   _Vcvv 2641

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-v 2643

This theorem is referenced by:  issetf  2648  isseti  2649  issetri  2650  elex  2652  elisset  2655  vtoclg1f  2700  ceqex  2766  eueq  2808  moeq  2812  mosubt  2814  ru  2861  sbc5  2885  snprc  3535  vprc  4000  opelopabsb  4120  eusvnfb  4313  euiotaex  5040  fvmptdf  5440  fvmptdv2  5442  fmptco  5518  brabvv  5749  ovmpodf  5834  ovi3  5839  tfrlemibxssdm  6154  tfr1onlembxssdm  6170  tfrcllembxssdm  6183  ecexr  6364  snexxph  6766  bj-vprc  12675  bj-vnex  12677  bj-2inf  12721