Theorem isset 2605

Description: Two ways to say " A is a set": A class A is a member of the universal class _V (see df-v 2603) 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 4192. Note the when A is not a set, it is called a proper class. In some theorems, such as uniexg 4193, 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 2077 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 2077	. 2 |- ( A e. _V <-> E. x ( x = A /\ x e. _V ) )
2		vex 2604	. . . 4 |- x e. _V
3	2	biantru 296	. . 3 |- ( x = A <-> ( x = A /\ x e. _V ) )
4	3	exbii 1536	. 2 |- ( E. x x = A <-> E. x ( x = A /\ x e. _V ) )
5	1, 4	bitr4i 185	1 |- ( A e. _V <-> E. x x = A )

Syntax hints:   /\ wa 102   <-> wb 103   = wceq 1284   E.wex 1421   e. wcel 1433   _Vcvv 2601

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-v 2603

This theorem is referenced by:  issetf  2606  isseti  2607  issetri  2608  elex  2610  elisset  2613  ceqex  2722  eueq  2763  moeq  2767  mosubt  2769  ru  2814  sbc5  2838  snprc  3457  vprc  3909  vnex  3911  opelopabsb  4015  eusvnfb  4204  euiotaex  4903  fvmptdf  5279  fvmptdv2  5281  fmptco  5351  brabvv  5571  ovmpt2df  5652  ovi3  5657  tfrlemibxssdm  5964  freccl  6016  ecexr  6134  bj-vprc  10687  bj-vnex  10689  bj-2inf  10733