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 4435. Note the when 𝐴 is not a set, it is called a proper class. In some theorems, such as uniexg 4437, 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  4133  opelopabsb  4258  eusvnfb  4452  elrelimasn  4991  euiotaex  5191  fvmptdf  5600  fvmptdv2  5602  fmptco  5679  brabvv  5916  ovmpodf  6001  ovi3  6006  tfrlemibxssdm  6323  tfr1onlembxssdm  6339  tfrcllembxssdm  6352  ecexr  6535  snexxph  6944  bj-vprc  14419  bj-vnex  14421  bj-2inf  14461
  Copyright terms: Public domain W3C validator