Theorem isset 3469

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem isset

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

Syntax hints:   ↔ wb 209   = wceq 1570  ∃wex 1809   ∈ wcel 2143  Vcvv 3455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457

This theorem is referenced by:  issetft  3471  issetri  3474  elex  3476  eueq  3671  ru  3743  sbc5ALT  3773  sbccomlem  3822  snprc  4683  snssb  4748  vprcOLD  5284  eusvnfb  5364  reusv2lem3  5371  fvmptd3f  7005  fvmptdv2  7008  ovmpodf  7566  rankf  9762  fnpr2ob  17607  isssc  17872  lrrecfr  28136  snelsingles  36412  bj-sbcex  37273  bj-inex1gALT  37560  bj-snglex  37609  bj-abex  37666  bj-clex  37667  bj-nul  37692  dissneqlem  37986  wl-issetft  38237  snen1g  44250  rr-spce  44928  iotaexeu  45128  elnev  45147  ax6e2nd  45267  ax6e2ndVD  45616  ax6e2ndALT  45638  upbdrech  46024  itgsubsticclem  46689