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

Theorem isset 2558
Description: Two ways to say "𝐴 is a set": A class 𝐴 is a member of the universal class V (see df-v 2556) 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 4170. Note the when 𝐴 is not a set, it is called a proper class. In some theorems, such as uniexg 4171, 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 2036 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 2036 . 2 (𝐴 ∈ V ↔ ∃𝑥(𝑥 = 𝐴𝑥 ∈ V))
2 vex 2557 . . . 4 𝑥 ∈ V
32biantru 286 . . 3 (𝑥 = 𝐴 ↔ (𝑥 = 𝐴𝑥 ∈ V))
43exbii 1496 . 2 (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴𝑥 ∈ V))
51, 4bitr4i 176 1 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wa 97  wb 98   = wceq 1243  wex 1381  wcel 1393  Vcvv 2554
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 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-v 2556
This theorem is referenced by:  issetf  2559  isseti  2560  issetri  2561  elex  2563  elisset  2565  ceqex  2668  eueq  2709  moeq  2713  mosubt  2715  ru  2760  sbc5  2784  snprc  3432  vprc  3885  vnex  3887  opelopabsb  3994  eusvnfb  4182  dtruex  4277  euiotaex  4870  fvmptdf  5245  fvmptdv2  5247  fmptco  5317  brabvv  5538  ovmpt2df  5619  ovi3  5624  tfrlemibxssdm  5928  freccl  5980  ecexr  6098  bj-vprc  9889  bj-vnex  9891  bj-2inf  9935
  Copyright terms: Public domain W3C validator