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

Theorem isset 3504
Description: Two ways to say "𝐴 is a set": A class 𝐴 is a member of the universal class V (see df-v 3494) 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 7454. Note that a class 𝐴 which is not a set is called a proper class. In some theorems, such as uniexg 7456, 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 2890 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 dfclel 2891 . 2 (𝐴 ∈ V ↔ ∃𝑥(𝑥 = 𝐴𝑥 ∈ V))
2 vex 3495 . . . 4 𝑥 ∈ V
32biantru 530 . . 3 (𝑥 = 𝐴 ↔ (𝑥 = 𝐴𝑥 ∈ V))
43exbii 1839 . 2 (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴𝑥 ∈ V))
51, 4bitr4i 279 1 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396   = wceq 1528  wex 1771  wcel 2105  Vcvv 3492
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-v 3494
This theorem is referenced by:  issetf  3505  issetiOLD  3507  issetri  3508  elex  3510  elissetOLD  3513  eueq  3696  ru  3768  sbc5  3797  snprc  4645  vprc  5210  eusvnfb  5284  reusv2lem3  5291  iotaex  6328  funimaexg  6433  fvmptd3f  6775  fvmptdv2  6778  ovmpodf  7295  rankf  9211  fnpr2ob  16819  isssc  17078  snelsingles  33280  bj-snglex  34182  bj-nul  34243  dissneqlem  34503  snen1g  39768  rr-spce  40435  iotaexeu  40627  elnev  40647  ax6e2nd  40769  ax6e2ndVD  41119  ax6e2ndALT  41141  upbdrech  41448  itgsubsticclem  42136
  Copyright terms: Public domain W3C validator