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

Theorem isset 3084
Description: Two ways to say "𝐴 is a set": A class 𝐴 is a member of the universal class V (see df-v 3079) 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 6726. Note the when 𝐴 is not a set, it is called a proper class. In some theorems, such as uniexg 6728, 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 2510 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 2510 . 2 (𝐴 ∈ V ↔ ∃𝑥(𝑥 = 𝐴𝑥 ∈ V))
2 vex 3080 . . . 4 𝑥 ∈ V
32biantru 524 . . 3 (𝑥 = 𝐴 ↔ (𝑥 = 𝐴𝑥 ∈ V))
43exbii 1752 . 2 (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴𝑥 ∈ V))
51, 4bitr4i 265 1 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 194  wa 382   = wceq 1474  wex 1694  wcel 1938  Vcvv 3077
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-12 1983  ax-ext 2494
This theorem depends on definitions:  df-bi 195  df-an 384  df-tru 1477  df-ex 1695  df-sb 1831  df-clab 2501  df-cleq 2507  df-clel 2510  df-v 3079
This theorem is referenced by:  issetf  3085  isseti  3086  issetri  3087  elex  3089  elisset  3092  vtoclg1f  3142  eueq  3249  moeq  3253  ru  3305  sbc5  3331  snprc  4100  vprc  4623  vnex  4625  eusvnfb  4687  reusv2lem3  4696  iotaex  5670  funimaexg  5774  fvmptdf  6087  fvmptdv2  6089  ovmpt2df  6566  rankf  8415  isssc  16193  snelsingles  31035  bj-snglex  31986  bj-nul  32041  dissneqlem  32195  iotaexeu  37523  elnev  37543  ax6e2nd  37677  ax6e2ndVD  38048  ax6e2ndALT  38070  upbdrech  38345  itgsubsticclem  38757
  Copyright terms: Public domain W3C validator