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

Theorem isset 3359
Description: Two ways to say "𝐴 is a set": A class 𝐴 is a member of the universal class V (see df-v 3353) 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 7098. Note that a class 𝐴 which is not a set is called a proper class. In some theorems, such as uniexg 7100, 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 2767 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 2767 . 2 (𝐴 ∈ V ↔ ∃𝑥(𝑥 = 𝐴𝑥 ∈ V))
2 vex 3354 . . . 4 𝑥 ∈ V
32biantru 519 . . 3 (𝑥 = 𝐴 ↔ (𝑥 = 𝐴𝑥 ∈ V))
43exbii 1924 . 2 (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴𝑥 ∈ V))
51, 4bitr4i 267 1 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 382   = wceq 1631  wex 1852  wcel 2145  Vcvv 3351
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-tru 1634  df-ex 1853  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-v 3353
This theorem is referenced by:  issetf  3360  isseti  3361  issetri  3362  elex  3364  elisset  3367  vtoclg1f  3416  eueq  3530  moeq  3534  ru  3586  sbc5  3612  snprc  4389  vprc  4931  eusvnfb  4993  reusv2lem3  5000  iotaex  6009  funimaexg  6113  fvmptd3f  6435  fvmptdv2  6438  ovmpt2df  6937  rankf  8819  isssc  16680  dmscut  32248  snelsingles  32359  bj-snglex  33285  bj-nul  33342  dissneqlem  33517  iotaexeu  39138  elnev  39158  ax6e2nd  39292  ax6e2ndVD  39659  ax6e2ndALT  39681  upbdrech  40029  itgsubsticclem  40701
  Copyright terms: Public domain W3C validator