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

Theorem isset 2863
Description: Two ways to say " is a set": A class is a member of the universal class (see df-v 2861) if and only if the class exists (i.e. there exists some set equal to class ). Theorem 6.9 of [Quine] p. 43. Notational convention: We will use the notational device " " to mean " is a set" very frequently, for example in uniex 4317. Note the when 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 instead of to mean " is a set."

Note that a constant is implicitly considered distinct from all variables. This is why is not included in the distinct variable list, even though df-clel 2349 requires that the expression substituted for not contain . (Also, the Metamath spec does not allow constants in the distinct variable list.) (Contributed by NM, 5-Aug-1993.)

Assertion
Ref Expression
isset
Distinct variable group:   ,

Proof of Theorem isset
StepHypRef Expression
1 df-clel 2349 . 2
2 vex 2862 . . . 4
32biantru 491 . . 3
43exbii 1582 . 2
51, 4bitr4i 243 1
Colors of variables: wff setvar class
Syntax hints:   wb 176   wa 358  wex 1541   wceq 1642   wcel 1710  cvv 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