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

Theorem isset 2538
Description: Two ways to say " is a set": A class is a member of the universal class  _V (see df-v 2536) 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 2019 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 2019 . 2  _V  _V
2 vex 2537 . . . 4 
_V
32biantru 286 . . 3  _V
43exbii 1480 . 2 
_V
51, 4bitr4i 176 1  _V
Colors of variables: wff set class
Syntax hints:   wa 97   wb 98  wex 1362   wceq 1374   wcel 1376   _Vcvv 2534
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 1316  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1378  ax-4 1383  ax-17 1402  ax-i9 1406  ax-ial 1411  ax-ext 2005
This theorem depends on definitions:  df-bi 110  df-sb 1629  df-clab 2010  df-cleq 2016  df-clel 2019  df-v 2536
This theorem is referenced by:  issetf  2539  isseti  2540  issetri  2541  elex  2542  elisset  2544  ceqex  2647  eueq  2688  moeq  2692  mosubt  2694  ru  2739  sbc5  2763  snprc  3387  vprc  3841  vnex  3843  opelopabsb  3951  eusvnfb  4112  dtruex  4197  euiotaex  4787  fvmptdf  5160  fvmptdv2  5162  fmptco  5232  brabvv  5453  ovmpt2df  5534  tfrlemibxssdm  5837  ecexr  5994
  Copyright terms: Public domain W3C validator