Theorem isset 2758

Description: Two ways to say " A is a set": A class A is a member of the universal class _V (see df-v 2754) 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 4452. Note the when A is not a set, it is called a proper class. In some theorems, such as uniexg 4454, 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 2185 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 2185	. 2 |- ( A e. _V <-> E. x ( x = A /\ x e. _V ) )
2		vex 2755	. . . 4 |- x e. _V
3	2	biantru 302	. . 3 |- ( x = A <-> ( x = A /\ x e. _V ) )
4	3	exbii 1616	. 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 1364   E.wex 1503   e. wcel 2160   _Vcvv 2752

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-v 2754

This theorem is referenced by:  issetf  2759  isseti  2760  issetri  2761  elex  2763  elisset  2766  vtoclg1f  2811  ceqex  2879  eueq  2923  moeq  2927  mosubt  2929  ru  2976  sbc5  3001  snprc  3672  snssb  3740  vprc  4150  opelopabsb  4275  eusvnfb  4469  elrelimasn  5009  euiotaex  5209  fvmptdf  5619  fvmptdv2  5621  fmptco  5698  brabvv  5937  ovmpodf  6023  ovi3  6028  tfrlemibxssdm  6346  tfr1onlembxssdm  6362  tfrcllembxssdm  6375  ecexr  6558  snexxph  6967  fnpr2ob  12782  bj-vprc  15045  bj-vnex  15047  bj-2inf  15087