Theorem isset 3450

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem isset

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

Syntax hints:   ↔ wb 206   = wceq 1541  ∃wex 1780   ∈ wcel 2111  Vcvv 3436

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438

This theorem is referenced by:  issetft  3452  issetri  3455  elex  3457  elexOLD  3458  eueq  3662  ru  3734  ruOLD  3735  sbc5ALT  3765  sbccomlem  3815  snprc  4665  snssb  4730  vprc  5248  eusvnfb  5326  reusv2lem3  5333  fvmptd3f  6939  fvmptdv2  6942  ovmpodf  7497  rankf  9682  fnpr2ob  17457  isssc  17722  lrrecfr  27881  snelsingles  35956  bj-snglex  37007  bj-abex  37064  bj-clex  37065  bj-nul  37090  dissneqlem  37374  wl-issetft  37616  snen1g  43557  rr-spce  44237  iotaexeu  44451  elnev  44470  ax6e2nd  44591  ax6e2ndVD  44940  ax6e2ndALT  44962  upbdrech  45346  itgsubsticclem  46013