Theorem isset 2573

Description: Two ways to say "A is a set": A class A is a member of the universal class _V (see df-v 2571) 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 3965. Note the when A is not a set, it is called a proper class. In some theorems, such as uniexg 3966, 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 2166 requires that the expression substituted for B not contain x. (Also, the Metamath spec does not allow constants in the distinct variable list.)

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 2166	. 2 |- (A e. _V <-> E.x(x = A /\ x e. _V))
2		visset 2572	. . . 4 |- x e. _V
3	2	biantru 999	. . 3 |- (x = A <-> (x = A /\ x e. _V))
4	3	exbii 1716	. 2 |- (E.x x = A <-> E.x(x = A /\ x e. _V))
5	1, 4	bitr4i 310	1 |- (A e. _V <-> E.x x = A)

Syntax hints:   <-> wb 231   /\ wa 433   = wceq 1615   e. wcel 1617  E.wex 1644  _Vcvv 2569

This theorem is referenced by:  issetf 2574  isseti 2576  issetri 2577  elisset 2578  elex 2580  vtoclgf 2618  cla4gf 2633  ceqex 2662  eueq 2703  moeq 2707  ru 2728  elrabsf 2756  snprc 3314  0ex 3646  vprc 3648  vnex 3650  pwex 3686  dmsnop 4510  funimaexg 4633  isarep2 4636  fopab2 4927  iotaex 5273  tz9.12lem1 6057  tz9.12lem3 6059  hashgval 8732  inficlALT 11205  fiuni 11212  fsubbas 11277  snelsingles 15023  fopab2g 15480  inficlALTOLD 16457  ceqsex3OLD 17334  iotaexeu 17467  elnev 17489  issetaOLD 17490

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1622  ax-12 1627  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-ext 2152

This theorem depends on definitions:  df-bi 232  df-an 435  df-ex 1645  df-sb 1845  df-clab 2158  df-cleq 2163  df-clel 2166  df-v 2571

Copyright terms: Public domain