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

Theorem isset 3179
Description: Two ways to say "𝐴 is a set": A class 𝐴 is a member of the universal class V (see df-v 3174) 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 6828. Note the when 𝐴 is not a set, it is called a proper class. In some theorems, such as uniexg 6830, 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 2605 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 2605 . 2 (𝐴 ∈ V ↔ ∃𝑥(𝑥 = 𝐴𝑥 ∈ V))
2 vex 3175 . . . 4 𝑥 ∈ V
32biantru 524 . . 3 (𝑥 = 𝐴 ↔ (𝑥 = 𝐴𝑥 ∈ V))
43exbii 1763 . 2 (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴𝑥 ∈ V))
51, 4bitr4i 265 1 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 194  wa 382   = wceq 1474  wex 1694  wcel 1976  Vcvv 3172
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-12 2033  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-an 384  df-tru 1477  df-ex 1695  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-v 3174
This theorem is referenced by:  issetf  3180  isseti  3181  issetri  3182  elex  3184  elisset  3187  vtoclg1f  3237  eueq  3344  moeq  3348  ru  3400  sbc5  3426  snprc  4196  vprc  4719  vnex  4721  eusvnfb  4783  reusv2lem3  4792  iotaex  5771  funimaexg  5875  fvmptdf  6189  fvmptdv2  6191  ovmpt2df  6668  rankf  8517  isssc  16249  snelsingles  31005  bj-snglex  31950  bj-nul  32005  dissneqlem  32159  iotaexeu  37437  elnev  37457  ax6e2nd  37591  ax6e2ndVD  37962  ax6e2ndALT  37984  upbdrech  38256  itgsubsticclem  38664
  Copyright terms: Public domain W3C validator