Theorem isset 3454

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem isset

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

Syntax hints:   ↔ wb 206   = wceq 1541  ∃wex 1780   ∈ wcel 2113  Vcvv 3440

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442

This theorem is referenced by:  issetft  3456  issetri  3459  elex  3461  elexOLD  3462  eueq  3666  ru  3738  ruOLD  3739  sbc5ALT  3769  sbccomlem  3819  snprc  4674  snssb  4739  vprc  5260  eusvnfb  5338  reusv2lem3  5345  fvmptd3f  6956  fvmptdv2  6959  ovmpodf  7514  rankf  9706  fnpr2ob  17479  isssc  17744  lrrecfr  27939  snelsingles  36114  bj-snglex  37174  bj-abex  37231  bj-clex  37232  bj-nul  37257  dissneqlem  37545  wl-issetft  37787  snen1g  43765  rr-spce  44445  iotaexeu  44659  elnev  44678  ax6e2nd  44799  ax6e2ndVD  45148  ax6e2ndALT  45170  upbdrech  45553  itgsubsticclem  46219