 New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  isset GIF version

Theorem isset 2863
 Description: Two ways to say "A is a set": A class A is a member of the universal class V (see df-v 2861) 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 ∈ V " to mean "A is a set" very frequently, for example in uniex 4317. Note the when A is not a set, it is called a proper class. In some theorems, such as uniexg 4316, in order to shorten certain proofs we use the more general antecedent A ∈ V instead of A ∈ 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 2349 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, 5-Aug-1993.)
Assertion
Ref Expression
isset (A V ↔ x x = A)
Distinct variable group:   x,A

Proof of Theorem isset
StepHypRef Expression
1 df-clel 2349 . 2 (A V ↔ x(x = A x V))
2 vex 2862 . . . 4 x V
32biantru 491 . . 3 (x = A ↔ (x = A x V))
43exbii 1582 . 2 (x x = Ax(x = A x V))
51, 4bitr4i 243 1 (A V ↔ x x = A)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 176   ∧ wa 358  ∃wex 1541   = wceq 1642   ∈ wcel 1710  Vcvv 2859 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334 This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-v 2861 This theorem is referenced by:  issetf  2864  isseti  2865  issetri  2866  elex  2867  elisset  2869  ceqex  2969  eueq  3008  moeq  3012  ru  3045  sbc5  3070  snprc  3788  ninexg  4097  snex  4111  1cex  4142  xpkvexg  4285  iotaex  4356  opeqexb  4620  eloprabga  5578  dmmpt  5683  fnce  6176
 Copyright terms: Public domain W3C validator