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

Theorem isset 3085
Description: Two ways to say " is a set": A class is a member of the universal class (see df-v 3083) 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 6509. Note the when is not a set, it is called a proper class. In some theorems, such as uniexg 6510, 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 2449 requires that the expression substituted for not contain . (Also, the Metamath spec does not allow constants in the distinct variable list.) (Contributed by NM, 26-May-1993.)

Assertion
Ref Expression
isset
Distinct variable group:   ,

Proof of Theorem isset
StepHypRef Expression
1 df-clel 2449 . 2
2 vex 3084 . . . 4
32biantru 505 . . 3
43exbii 1635 . 2
51, 4bitr4i 252 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369  =wceq 1370  E.wex 1587  e.wcel 1758   cvv 3081
This theorem is referenced by:  issetf  3086  isseti  3087  issetri  3088  elex  3090  elisset  3092  vtoclg1f  3138  eueq  3241  moeq  3245  ru  3296  sbc5  3322  snprc  4056  vprc  4547  vnex  4549  eusvnfb  4605  reusv2lem3  4612  iotaex  5517  funimaexg  5614  fvmptdf  5908  fvmptdv2  5910  ovmpt2df  6355  rankf  8138  isssc  14892  snelsingles  28409  ceqsex3OLD  29465  iotaexeu  30132  elnev  30152  upbdrech  30311  itgsubsticclem  30522  ax6e2nd  32110  ax6e2ndVD  32487  ax6e2ndALT  32509  bj-snglex  33311  bj-nul  33365
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-12 1794  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-v 3083
  Copyright terms: Public domain W3C validator