Theorem isset 2745

Description: Two ways to say " A is a set": A class A is a member of the universal class _V (see df-v 2741) 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 4439. Note the when A is not a set, it is called a proper class. In some theorems, such as uniexg 4441, 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 2173 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 2173	. 2 |- ( A e. _V <-> E. x ( x = A /\ x e. _V ) )
2		vex 2742	. . . 4 |- x e. _V
3	2	biantru 302	. . 3 |- ( x = A <-> ( x = A /\ x e. _V ) )
4	3	exbii 1605	. 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 1353   E.wex 1492   e. wcel 2148   _Vcvv 2739

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-v 2741

This theorem is referenced by:  issetf  2746  isseti  2747  issetri  2748  elex  2750  elisset  2753  vtoclg1f  2798  ceqex  2866  eueq  2910  moeq  2914  mosubt  2916  ru  2963  sbc5  2988  snprc  3659  snssb  3727  vprc  4137  opelopabsb  4262  eusvnfb  4456  elrelimasn  4996  euiotaex  5196  fvmptdf  5605  fvmptdv2  5607  fmptco  5684  brabvv  5923  ovmpodf  6008  ovi3  6013  tfrlemibxssdm  6330  tfr1onlembxssdm  6346  tfrcllembxssdm  6359  ecexr  6542  snexxph  6951  fnpr2ob  12764  bj-vprc  14687  bj-vnex  14689  bj-2inf  14729