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

Theorem isset 3197
Description: Two ways to say "𝐴 is a set": A class 𝐴 is a member of the universal class V (see df-v 3192) 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 6918. Note the when 𝐴 is not a set, it is called a proper class. In some theorems, such as uniexg 6920, 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 3193 . . . 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 3190
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 3192
This theorem is referenced by:  issetf  3198  isseti  3199  issetri  3200  elex  3202  elisset  3205  vtoclg1f  3255  eueq  3365  moeq  3369  ru  3421  sbc5  3447  snprc  4230  vprc  4766  vnex  4768  eusvnfb  4832  reusv2lem3  4841  iotaex  5837  funimaexg  5943  fvmptdf  6262  fvmptdv2  6264  ovmpt2df  6757  rankf  8617  isssc  16420  snelsingles  31724  bj-snglex  32661  bj-nul  32718  dissneqlem  32858  iotaexeu  38140  elnev  38160  ax6e2nd  38295  ax6e2ndVD  38666  ax6e2ndALT  38688  upbdrech  39018  itgsubsticclem  39528
  Copyright terms: Public domain W3C validator