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

Theorem isset 2445
Description: Two ways to say "A is a set": A class A is a member of the universal class V (see df-v 2443) 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 1941 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 1941 . 2 (A V ↔ x(x = A x V))
2 vex 2444 . . . 4 x V
32biantru 284 . . 3 (x = A ↔ (x = A x V))
43exbii 1442 . 2 (x x = Ax(x = A x V))
51, 4bitr4i 174 1 (A V ↔ x x = A)
Colors of variables: wff set class
Syntax hints:   wa 95  wb 96  wex 1328   = wceq 1340   wcel 1342  Vcvv 2441
This theorem is referenced by:  issetf  2446  isseti  2447  issetri  2448  elex  2449  elisset  2451  ceqex  2553  eueq  2593  moeq  2597  ru  2643  sbc5  2667
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 97  ax-ia2 98  ax-ia3 99  ax-5 1282  ax-gen 1284  ax-ie1 1329  ax-ie2 1330  ax-8 1344  ax-4 1349  ax-17 1367  ax-i9 1371  ax-ial 1376  ax-ext 1928
This theorem depends on definitions:  df-bi 108  df-sb 1586  df-clab 1932  df-cleq 1938  df-clel 1941  df-v 2443
  Copyright terms: Public domain W3C validator