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

Theorem isset 2536
Description: Two ways to say "A is a set": A class A is a member of the universal class V (see df-v 2534) if and only if the class A exists (i.e. there exists some set x equal to class A). Theorem 6.9 of [Quine] p. 43. Notational convention: We will use the notational device "A V " to mean "A is a set" very frequently, for example in uniex . Note the when A 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 A 𝑉 instead of A V to mean "A 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 2017 requires that the expression substituted for B not contain x. (Also, the Metamath spec does not allow constants in the distinct variable list.) (Contributed by NM, 5-Aug-1993.)

Assertion
Ref Expression
isset (A V ↔ x x = A)
Distinct variable group:   x,A

Proof of Theorem isset
StepHypRef Expression
1 df-clel 2017 . 2 (A V ↔ x(x = A x V))
2 vex 2535 . . . 4 x V
32biantru 286 . . 3 (x = A ↔ (x = A x V))
43exbii 1480 . 2 (x x = Ax(x = A x V))
51, 4bitr4i 176 1 (A V ↔ x x = A)
Colors of variables: wff set class
Syntax hints:   wa 97  wb 98   = wceq 1230  wex 1364   wcel 1376  Vcvv 2532
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 1318  ax-gen 1320  ax-ie1 1365  ax-ie2 1366  ax-8 1378  ax-4 1383  ax-17 1402  ax-i9 1406  ax-ial 1411  ax-ext 2003
This theorem depends on definitions:  df-bi 110  df-sb 1629  df-clab 2008  df-cleq 2014  df-clel 2017  df-v 2534
This theorem is referenced by:  issetf  2537  isseti  2538  issetri  2539  elex  2540  elisset  2542  ceqex  2645  eueq  2686  moeq  2690  mosubt  2692  ru  2737  sbc5  2761  snprc  3382  vprc  3835  vnex  3837  opelopabsb  3944  eusvnfb  4107  dtruex  4192  euiotaex  4781  fvmptdf  5154  fvmptdv2  5156  fmptco  5226  brabvv  5445  ovmpt2df  5526  ovi3  5531  tfrlemibxssdm  5830  ecexr  5987
  Copyright terms: Public domain W3C validator