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

Theorem isset 2955
Description: Two ways to say " is a set": A class is a member of the universal class (see df-v 2953) 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 6346. Note the when is not a set, it is called a proper class. In some theorems, such as uniexg 6347, 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 2418 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 2418 . 2
2 vex 2954 . . . 4
32biantru 495 . . 3
43exbii 1626 . 2
51, 4bitr4i 246 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 178  /\wa 362  E.wex 1581  =wceq 1687  e.wcel 1749   cvv 2951
This theorem is referenced by:  issetf  2956  isseti  2957  issetri  2958  elex  2960  elisset  2962  vtoclg1f  3007  eueq  3109  moeq  3113  ru  3163  sbc5  3188  snprc  3916  vprc  4405  vnex  4407  eusvnfb  4460  reusv2lem3  4467  iotaex  5370  funimaexg  5465  fvmptdf  5755  fvmptdv2  5757  ovmpt2df  6192  rankf  7948  isssc  14673  snelsingles  27655  ceqsex3OLD  28677  iotaexeu  29345  elnev  29365  ax6e2nd  30844  ax6e2ndVD  31222  ax6e2ndALT  31244  bj-snglex  31913
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-12 1785  ax-ext 2403
This theorem depends on definitions:  df-bi 179  df-an 364  df-ex 1582  df-sb 1694  df-clab 2409  df-cleq 2415  df-clel 2418  df-v 2953
  Copyright terms: Public domain W3C validator