Theorem isset 3445

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem isset

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

Syntax hints:   ↔ wb 207   = wceq 1547  ∃wex 1786   ∈ wcel 2119  Vcvv 3431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433

This theorem is referenced by:  issetft  3447  issetri  3450  elex  3452  eueq  3649  ru  3721  ruOLD  3722  sbc5ALT  3752  sbccomlem  3801  snprc  4649  snssb  4714  vprcOLD  5243  eusvnfb  5322  reusv2lem3  5329  fvmptd3f  6951  fvmptdv2  6954  ovmpodf  7512  rankf  9709  fnpr2ob  17513  isssc  17778  lrrecfr  27953  snelsingles  36148  bj-sbcex  36991  bj-snglex  37326  bj-abex  37383  bj-clex  37384  bj-nul  37409  dissneqlem  37702  wl-issetft  37953  snen1g  43968  rr-spce  44648  iotaexeu  44862  elnev  44881  ax6e2nd  45002  ax6e2ndVD  45351  ax6e2ndALT  45373  upbdrech  45753  itgsubsticclem  46418