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

Theorem isset 2526
Description: Two ways to say " is a set": A class is a member of the universal class  _V (see df-v 2524) 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 "  _V " to mean " is a set" very frequently, for example in uniex . Note the when is not a set, it is called a proper class. In some theorems, such as uniexg , in order to shorten certain proofs we use the more general antecedent  V instead of  _V to mean " is a set."

Note that a constant is implicitly considered distinct from all variables. This is why  _V is not included in the distinct variable list, even though df-clel 2005 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  _V
Distinct variable group:   ,

Proof of Theorem isset
StepHypRef Expression
1 df-clel 2005 . 2  _V  _V
2 vex 2525 . . . 4 
_V
32biantru 286 . . 3  _V
43exbii 1465 . 2 
_V
51, 4bitr4i 176 1  _V
Colors of variables: wff set class
Syntax hints:   wa 97   wb 98   wceq 1219  wex 1350   wcel 1362   _Vcvv 2522
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 1305  ax-gen 1307  ax-ie1 1351  ax-ie2 1352  ax-8 1364  ax-4 1369  ax-17 1388  ax-i9 1392  ax-ial 1396  ax-ext 1991
This theorem depends on definitions:  df-bi 110  df-sb 1615  df-clab 1996  df-cleq 2002  df-clel 2005  df-v 2524
This theorem is referenced by:  issetf  2527  isseti  2528  issetri  2529  elex  2530  elisset  2532  ceqex  2635  eueq  2676  moeq  2680  mosubt  2682  ru  2727  sbc5  2751  snprc  3394  vprc  3847  vnex  3849  opelopabsb  3956  eusvnfb  4120  dtruex  4205  euiotaex  4794  fvmptdf  5167  fvmptdv2  5169  fmptco  5239  brabvv  5458  ovmpt2df  5539  ovi3  5544  tfrlemibxssdm  5846  ecexr  6006  bj-vprc  7353  bj-vnex  7355  bj-2inf  7398
  Copyright terms: Public domain W3C validator