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

Theorem isset 2616
Description: Two ways to say "𝐴 is a set": A class 𝐴 is a member of the universal class V (see df-v 2614) 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 4228. Note the when 𝐴 is not a set, it is called a proper class. In some theorems, such as uniexg 4229, 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 2079 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 2079 . 2 (𝐴 ∈ V ↔ ∃𝑥(𝑥 = 𝐴𝑥 ∈ V))
2 vex 2615 . . . 4 𝑥 ∈ V
32biantru 296 . . 3 (𝑥 = 𝐴 ↔ (𝑥 = 𝐴𝑥 ∈ V))
43exbii 1537 . 2 (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴𝑥 ∈ V))
51, 4bitr4i 185 1 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wa 102  wb 103   = wceq 1285  wex 1422  wcel 1434  Vcvv 2612
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-v 2614
This theorem is referenced by:  issetf  2617  isseti  2618  issetri  2619  elex  2621  elisset  2624  ceqex  2732  eueq  2774  moeq  2778  mosubt  2780  ru  2825  sbc5  2849  snprc  3481  vprc  3936  opelopabsb  4051  eusvnfb  4240  euiotaex  4950  fvmptdf  5335  fvmptdv2  5337  fmptco  5406  brabvv  5630  ovmpt2df  5711  ovi3  5716  tfrlemibxssdm  6024  tfr1onlembxssdm  6040  tfrcllembxssdm  6053  ecexr  6227  snexxph  6583  bj-vprc  11130  bj-vnex  11132  bj-2inf  11176
  Copyright terms: Public domain W3C validator