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

Theorem isset 3476
Description: Two ways to express that "𝐴 is a set": A class 𝐴 is a member of the universal class V (see df-v 3464) if and only if the class 𝐴 exists (i.e., there exists some set 𝑥 equal to class 𝐴). Theorem 6.9 of [Quine] p. 43.

A class 𝐴 which is not a set is called a proper class.

Conventions: We will often use the expression "𝐴 ∈ V " to mean "𝐴 is a set", for example in uniex 7744. To make some theorems more readily applicable, we will also use the more general expression 𝐴𝑉 instead of 𝐴 ∈ V to mean "𝐴 is a set", typically in an antecedent, or in a hypothesis for theorems in deduction form (see for instance uniexg 7743 compared with uniex 7744). That this is more general is seen either by substitution (when the variable 𝑉 has no other occurrences), or by elex 3482. (Contributed by NM, 26-May-1993.)

Assertion
Ref Expression
isset (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
Distinct variable group:   𝑥,𝐴

Proof of Theorem isset
StepHypRef Expression
1 vex 3466 . 2 𝑥 ∈ V
21issetlem 2806 1 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1534  wex 1774  wcel 2099  Vcvv 3462
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464
This theorem is referenced by:  issetft  3477  issetri  3480  elex  3482  elexOLD  3483  eueq  3701  ru  3773  ruOLD  3774  sbc5ALT  3804  snprc  4716  snssb  4781  vprc  5312  eusvnfb  5389  reusv2lem3  5396  iotaexOLD  6526  funimaexgOLD  6638  fvmptd3f  7016  fvmptdv2  7019  ovmpodf  7574  rankf  9830  fnpr2ob  17568  isssc  17831  lrrecfr  27954  snelsingles  35759  bj-snglex  36693  bj-abex  36750  bj-clex  36751  bj-nul  36776  dissneqlem  37060  wl-issetft  37290  snen1g  43228  rr-spce  43908  iotaexeu  44129  elnev  44149  ax6e2nd  44271  ax6e2ndVD  44621  ax6e2ndALT  44643  upbdrech  44956  itgsubsticclem  45632
  Copyright terms: Public domain W3C validator