Theorem isset 3473

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem isset

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

Syntax hints:   ↔ wb 206   = wceq 1540  ∃wex 1779   ∈ wcel 2108  Vcvv 3459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461

This theorem is referenced by:  issetft  3475  issetri  3478  elex  3480  elexOLD  3481  eueq  3691  ru  3763  ruOLD  3764  sbc5ALT  3794  sbccomlem  3844  snprc  4693  snssb  4758  vprc  5285  eusvnfb  5363  reusv2lem3  5370  iotaexOLD  6510  funimaexgOLD  6623  fvmptd3f  7000  fvmptdv2  7003  ovmpodf  7561  rankf  9806  fnpr2ob  17570  isssc  17831  lrrecfr  27893  snelsingles  35886  bj-snglex  36937  bj-abex  36994  bj-clex  36995  bj-nul  37020  dissneqlem  37304  wl-issetft  37546  snen1g  43495  rr-spce  44175  iotaexeu  44390  elnev  44410  ax6e2nd  44531  ax6e2ndVD  44880  ax6e2ndALT  44902  upbdrech  45282  itgsubsticclem  45952