Theorem isset 3444

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem isset

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432

This theorem is referenced by:  issetft  3446  issetri  3449  elex  3451  elexOLD  3452  eueq  3655  ru  3727  ruOLD  3728  sbc5ALT  3758  sbccomlem  3808  snprc  4662  snssb  4727  vprc  5252  eusvnfb  5330  reusv2lem3  5337  fvmptd3f  6957  fvmptdv2  6960  ovmpodf  7516  rankf  9709  fnpr2ob  17513  isssc  17778  lrrecfr  27949  snelsingles  36118  bj-sbcex  36961  bj-snglex  37296  bj-abex  37353  bj-clex  37354  bj-nul  37379  dissneqlem  37670  wl-issetft  37921  snen1g  43969  rr-spce  44649  iotaexeu  44863  elnev  44882  ax6e2nd  45003  ax6e2ndVD  45352  ax6e2ndALT  45374  upbdrech  45756  itgsubsticclem  46421