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

Theorem isset 2743
Description: Two ways to say "𝐴 is a set": A class 𝐴 is a member of the universal class V (see df-v 2739) 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 4436. Note the when 𝐴 is not a set, it is called a proper class. In some theorems, such as uniexg 4438, 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 2173 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 2173 . 2 (𝐴 ∈ V ↔ ∃𝑥(𝑥 = 𝐴𝑥 ∈ V))
2 vex 2740 . . . 4 𝑥 ∈ V
32biantru 302 . . 3 (𝑥 = 𝐴 ↔ (𝑥 = 𝐴𝑥 ∈ V))
43exbii 1605 . 2 (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴𝑥 ∈ V))
51, 4bitr4i 187 1 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wa 104  wb 105   = wceq 1353  wex 1492  wcel 2148  Vcvv 2737
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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-v 2739
This theorem is referenced by:  issetf  2744  isseti  2745  issetri  2746  elex  2748  elisset  2751  vtoclg1f  2796  ceqex  2864  eueq  2908  moeq  2912  mosubt  2914  ru  2961  sbc5  2986  snprc  3657  snssb  3725  vprc  4134  opelopabsb  4259  eusvnfb  4453  elrelimasn  4992  euiotaex  5192  fvmptdf  5601  fvmptdv2  5603  fmptco  5680  brabvv  5917  ovmpodf  6002  ovi3  6007  tfrlemibxssdm  6324  tfr1onlembxssdm  6340  tfrcllembxssdm  6353  ecexr  6536  snexxph  6945  bj-vprc  14499  bj-vnex  14501  bj-2inf  14541
  Copyright terms: Public domain W3C validator