Theorem isset 3477

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem isset

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

Syntax hints:   ↔ wb 209   = wceq 1567  ∃wex 1806   ∈ wcel 2149  Vcvv 3463

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465

This theorem is referenced by:  issetft  3479  issetri  3482  elex  3484  eueq  3680  ru  3752  sbc5ALT  3782  sbccomlem  3831  snprc  4685  snssb  4750  vprcOLD  5283  eusvnfb  5362  reusv2lem3  5369  fvmptd3f  7003  fvmptdv2  7006  ovmpodf  7564  rankf  9762  fnpr2ob  17608  isssc  17873  lrrecfr  28098  snelsingles  36307  bj-sbcex  37158  bj-snglex  37493  bj-abex  37550  bj-clex  37551  bj-nul  37576  dissneqlem  37869  wl-issetft  38120  snen1g  44137  rr-spce  44815  iotaexeu  45015  elnev  45034  ax6e2nd  45154  ax6e2ndVD  45503  ax6e2ndALT  45525  upbdrech  45911  itgsubsticclem  46576