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

Theorem isset 2758
Description: Two ways to say "𝐴 is a set": A class 𝐴 is a member of the universal class V (see df-v 2754) 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 4455. Note the when 𝐴 is not a set, it is called a proper class. In some theorems, such as uniexg 4457, in order to shorten certain proofs we use the more general antecedent 𝐴𝑉 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 2185 requires that the expression substituted for 𝐵 not contain 𝑥. (Also, the Metamath spec does not allow constants in the distinct variable list.) (Contributed by NM, 26-May-1993.)

Assertion
Ref Expression
isset (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
Distinct variable group:   𝑥,𝐴

Proof of Theorem isset
StepHypRef Expression
1 df-clel 2185 . 2 (𝐴 ∈ V ↔ ∃𝑥(𝑥 = 𝐴𝑥 ∈ V))
2 vex 2755 . . . 4 𝑥 ∈ V
32biantru 302 . . 3 (𝑥 = 𝐴 ↔ (𝑥 = 𝐴𝑥 ∈ V))
43exbii 1616 . 2 (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴𝑥 ∈ V))
51, 4bitr4i 187 1 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wa 104  wb 105   = wceq 1364  wex 1503  wcel 2160  Vcvv 2752
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-ext 2171
This theorem depends on definitions:  df-bi 117  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-v 2754
This theorem is referenced by:  issetf  2759  isseti  2760  issetri  2761  elex  2763  elisset  2766  vtoclg1f  2811  ceqex  2879  eueq  2923  moeq  2927  mosubt  2929  ru  2976  sbc5  3001  snprc  3672  snssb  3740  vprc  4150  opelopabsb  4278  eusvnfb  4472  elrelimasn  5012  euiotaex  5212  fvmptdf  5624  fvmptdv2  5626  fmptco  5703  brabvv  5942  ovmpodf  6028  ovi3  6033  tfrlemibxssdm  6352  tfr1onlembxssdm  6368  tfrcllembxssdm  6381  ecexr  6564  snexxph  6979  fnpr2ob  12816  bj-vprc  15109  bj-vnex  15111  bj-2inf  15151
  Copyright terms: Public domain W3C validator