Theorem isset 3456

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem isset

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

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

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 3444

This theorem is referenced by:  issetft  3458  issetri  3461  elex  3463  elexOLD  3464  eueq  3668  ru  3740  ruOLD  3741  sbc5ALT  3771  sbccomlem  3821  snprc  4676  snssb  4741  vprc  5262  eusvnfb  5340  reusv2lem3  5347  fvmptd3f  6965  fvmptdv2  6968  ovmpodf  7524  rankf  9718  fnpr2ob  17491  isssc  17756  lrrecfr  27951  snelsingles  36136  bj-snglex  37221  bj-abex  37278  bj-clex  37279  bj-nul  37304  dissneqlem  37595  wl-issetft  37837  snen1g  43880  rr-spce  44560  iotaexeu  44774  elnev  44793  ax6e2nd  44914  ax6e2ndVD  45263  ax6e2ndALT  45285  upbdrech  45667  itgsubsticclem  46333