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

Theorem isset 3335
Description: Two ways to say "𝐴 is a set": A class 𝐴 is a member of the universal class V (see df-v 3330) 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 7106. Note that a class 𝐴 which is not a set is called a proper class. In some theorems, such as uniexg 7108, 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 2744 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 2744 . 2 (𝐴 ∈ V ↔ ∃𝑥(𝑥 = 𝐴𝑥 ∈ V))
2 vex 3331 . . . 4 𝑥 ∈ V
32biantru 527 . . 3 (𝑥 = 𝐴 ↔ (𝑥 = 𝐴𝑥 ∈ V))
43exbii 1911 . 2 (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴𝑥 ∈ V))
51, 4bitr4i 267 1 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383   = wceq 1620  wex 1841  wcel 2127  Vcvv 3328
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-12 2184  ax-ext 2728
This theorem depends on definitions:  df-bi 197  df-an 385  df-tru 1623  df-ex 1842  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-v 3330
This theorem is referenced by:  issetf  3336  isseti  3337  issetri  3338  elex  3340  elisset  3343  vtoclg1f  3393  eueq  3507  moeq  3511  ru  3563  sbc5  3589  snprc  4385  vprc  4936  vnex  4938  eusvnfb  4999  reusv2lem3  5008  iotaex  6017  funimaexg  6124  fvmptd3f  6445  fvmptdv2  6448  ovmpt2df  6945  rankf  8818  isssc  16652  dmscut  32195  snelsingles  32306  bj-snglex  33238  bj-nul  33295  dissneqlem  33469  iotaexeu  39090  elnev  39110  ax6e2nd  39245  ax6e2ndVD  39612  ax6e2ndALT  39634  upbdrech  39987  itgsubsticclem  40663
  Copyright terms: Public domain W3C validator