Theorem isset 3458

Description: Two ways to express that "𝐴 is a set": A class 𝐴 is a member of the universal class V (see df-v 3446) 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 7697. 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 7696 compared with uniex 7697). That this is more general is seen either by substitution (when the variable 𝑉 has no other occurrences), or by elex 3465. (Contributed by NM, 26-May-1993.)

Assertion

Ref	Expression
isset	⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)

Distinct variable group:   𝑥,𝐴

Proof of Theorem isset

Step	Hyp	Ref	Expression
1		vex 3448	. 2 ⊢ 𝑥 ∈ V
2	1	issetlem 2808	1 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)

Syntax hints:   ↔ wb 206   = wceq 1540  ∃wex 1779   ∈ wcel 2109  Vcvv 3444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446

This theorem is referenced by:  issetft  3460  issetri  3463  elex  3465  elexOLD  3466  eueq  3676  ru  3748  ruOLD  3749  sbc5ALT  3779  sbccomlem  3829  snprc  4677  snssb  4742  vprc  5265  eusvnfb  5343  reusv2lem3  5350  iotaexOLD  6479  fvmptd3f  6965  fvmptdv2  6968  ovmpodf  7525  rankf  9723  fnpr2ob  17497  isssc  17758  lrrecfr  27826  snelsingles  35883  bj-snglex  36934  bj-abex  36991  bj-clex  36992  bj-nul  37017  dissneqlem  37301  wl-issetft  37543  snen1g  43486  rr-spce  44166  iotaexeu  44380  elnev  44400  ax6e2nd  44521  ax6e2ndVD  44870  ax6e2ndALT  44892  upbdrech  45276  itgsubsticclem  45946