Theorem isset 3464

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem isset

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452

This theorem is referenced by:  issetft  3466  issetri  3469  elex  3471  elexOLD  3472  eueq  3682  ru  3754  ruOLD  3755  sbc5ALT  3785  sbccomlem  3835  snprc  4684  snssb  4749  vprc  5273  eusvnfb  5351  reusv2lem3  5358  iotaexOLD  6494  funimaexgOLD  6607  fvmptd3f  6986  fvmptdv2  6989  ovmpodf  7548  rankf  9754  fnpr2ob  17528  isssc  17789  lrrecfr  27857  snelsingles  35917  bj-snglex  36968  bj-abex  37025  bj-clex  37026  bj-nul  37051  dissneqlem  37335  wl-issetft  37577  snen1g  43520  rr-spce  44200  iotaexeu  44414  elnev  44434  ax6e2nd  44555  ax6e2ndVD  44904  ax6e2ndALT  44926  upbdrech  45310  itgsubsticclem  45980