MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isset Structured version   Visualization version   GIF version

Theorem isset 3193
Description: Two ways to say "𝐴 is a set": A class 𝐴 is a member of the universal class V (see df-v 3188) 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 6906. Note the when 𝐴 is not a set, it is called a proper class. In some theorems, such as uniexg 6908, 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 2617 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 2617 . 2 (𝐴 ∈ V ↔ ∃𝑥(𝑥 = 𝐴𝑥 ∈ V))
2 vex 3189 . . . 4 𝑥 ∈ V
32biantru 526 . . 3 (𝑥 = 𝐴 ↔ (𝑥 = 𝐴𝑥 ∈ V))
43exbii 1771 . 2 (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴𝑥 ∈ V))
51, 4bitr4i 267 1 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384   = wceq 1480  wex 1701  wcel 1987  Vcvv 3186
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-12 2044  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-tru 1483  df-ex 1702  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-v 3188
This theorem is referenced by:  issetf  3194  isseti  3195  issetri  3196  elex  3198  elisset  3201  vtoclg1f  3251  eueq  3360  moeq  3364  ru  3416  sbc5  3442  snprc  4223  vprc  4756  vnex  4758  eusvnfb  4822  reusv2lem3  4831  iotaex  5827  funimaexg  5933  fvmptdf  6252  fvmptdv2  6254  ovmpt2df  6745  rankf  8601  isssc  16401  snelsingles  31668  bj-snglex  32605  bj-nul  32662  dissneqlem  32816  iotaexeu  38098  elnev  38118  ax6e2nd  38253  ax6e2ndVD  38624  ax6e2ndALT  38646  upbdrech  38980  itgsubsticclem  39495
  Copyright terms: Public domain W3C validator