Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  isset Unicode version

Theorem isset 2920
 Description: Two ways to say " is a set": A class is a member of the universal class (see df-v 2918) 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 4664. Note the when is not a set, it is called a proper class. In some theorems, such as uniexg 4665, 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 2400 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 2400 . 2
2 vex 2919 . . . 4
32biantru 492 . . 3
43exbii 1589 . 2
51, 4bitr4i 244 1
 Colors of variables: wff set class Syntax hints:   wb 177   wa 359  wex 1547   wceq 1649   wcel 1721  cvv 2916 This theorem is referenced by:  issetf  2921  isseti  2922  issetri  2923  elex  2924  elisset  2926  ceqex  3026  eueq  3066  moeq  3070  ru  3120  sbc5  3145  snprc  3831  vprc  4301  vnex  4303  eusvnfb  4678  reusv2lem3  4685  iotaex  5394  funimaexg  5489  fvmptdf  5775  fvmptdv2  5777  ovmpt2df  6164  rankf  7676  isssc  13975  snelsingles  25675  ceqsex3OLD  26599  iotaexeu  27486  elnev  27506  a9e2nd  28356  a9e2ndVD  28729  a9e2ndALT  28752 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385 This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-v 2918
 Copyright terms: Public domain W3C validator