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

Theorem isset 2864
Description: Two ways to say " is a set": A class is a member of the universal class (see df-v 2862) 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 4318. Note the when is not a set, it is called a proper class. In some theorems, such as uniexg 4317, 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 2863 . . . 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 2860
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 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 2862
This theorem is referenced by:  issetf  2865  isseti  2866  issetri  2867  elex  2868  elisset  2870  ceqex  2970  eueq  3009  moeq  3013  ru  3046  sbc5  3071  snprc  3789  ninexg  4098  snex  4112  1cex  4143  xpkvexg  4286  iotaex  4357  opeqexb  4621  eloprabga  5579  dmmpt  5684  fnce  6177
  Copyright terms: Public domain W3C validator