Theorem isset 3443

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem isset

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

Syntax hints:   ↔ wb 206   = wceq 1542  ∃wex 1781   ∈ wcel 2114  Vcvv 3429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431

This theorem is referenced by:  issetft  3445  issetri  3448  elex  3450  elexOLD  3451  eueq  3654  ru  3726  ruOLD  3727  sbc5ALT  3757  sbccomlem  3807  snprc  4661  snssb  4726  vprcOLD  5256  eusvnfb  5335  reusv2lem3  5342  fvmptd3f  6963  fvmptdv2  6966  ovmpodf  7523  rankf  9718  fnpr2ob  17522  isssc  17787  lrrecfr  27935  snelsingles  36102  bj-sbcex  36945  bj-snglex  37280  bj-abex  37337  bj-clex  37338  bj-nul  37363  dissneqlem  37656  wl-issetft  37907  snen1g  43951  rr-spce  44631  iotaexeu  44845  elnev  44864  ax6e2nd  44985  ax6e2ndVD  45334  ax6e2ndALT  45356  upbdrech  45738  itgsubsticclem  46403