Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  isset Unicode version

Theorem isset 2561
 Description: Two ways to say " is a set": A class is a member of the universal class (see df-v 2559) 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 4174. Note the when is not a set, it is called a proper class. In some theorems, such as uniexg 4175, 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 2036 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 2036 . 2
2 vex 2560 . . . 4
32biantru 286 . . 3
43exbii 1496 . 2
51, 4bitr4i 176 1
 Colors of variables: wff set class Syntax hints:   wa 97   wb 98   wceq 1243  wex 1381   wcel 1393  cvv 2557 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-ext 2022 This theorem depends on definitions:  df-bi 110  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-v 2559 This theorem is referenced by:  issetf  2562  isseti  2563  issetri  2564  elex  2566  elisset  2568  ceqex  2671  eueq  2712  moeq  2716  mosubt  2718  ru  2763  sbc5  2787  snprc  3435  vprc  3888  vnex  3890  opelopabsb  3997  eusvnfb  4186  dtruex  4283  euiotaex  4883  fvmptdf  5258  fvmptdv2  5260  fmptco  5330  brabvv  5551  ovmpt2df  5632  ovi3  5637  tfrlemibxssdm  5941  freccl  5993  ecexr  6111  bj-vprc  10016  bj-vnex  10018  bj-2inf  10062
 Copyright terms: Public domain W3C validator