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

Theorem isset 2537
Description: Two ways to say "A is a set": A class A is a member of the universal class V (see df-v 2535) 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 2018 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 2018 . 2 (A V ↔ x(x = A x V))
2 vex 2536 . . . 4 x V
32biantru 286 . . 3 (x = A ↔ (x = A x V))
43exbii 1479 . 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  wex 1361   = wceq 1373   wcel 1375  Vcvv 2533
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 1315  ax-gen 1317  ax-ie1 1362  ax-ie2 1363  ax-8 1377  ax-4 1382  ax-17 1401  ax-i9 1405  ax-ial 1410  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-sb 1628  df-clab 2009  df-cleq 2015  df-clel 2018  df-v 2535
This theorem is referenced by:  issetf  2538  isseti  2539  issetri  2540  elex  2541  elisset  2543  ceqex  2646  eueq  2687  moeq  2691  mosubt  2693  ru  2738  sbc5  2762  snprc  3386  vprc  3840  vnex  3842  opelopabsb  3950  eusvnfb  4109  dtruex  4191  euiotaex  4777  fvmptdf  5150  fvmptdv2  5152  fmptco  5222  brabvv  5443  ovmpt2df  5524  tfrlemibxssdm  5827
  Copyright terms: Public domain W3C validator