Theorem isset 3494

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem isset

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482

This theorem is referenced by:  issetft  3496  issetri  3499  elex  3501  elexOLD  3502  eueq  3714  ru  3786  ruOLD  3787  sbc5ALT  3817  sbccomlem  3869  snprc  4717  snssb  4782  vprc  5315  eusvnfb  5393  reusv2lem3  5400  iotaexOLD  6541  funimaexgOLD  6654  fvmptd3f  7031  fvmptdv2  7034  ovmpodf  7589  rankf  9834  fnpr2ob  17603  isssc  17864  lrrecfr  27976  snelsingles  35923  bj-snglex  36974  bj-abex  37031  bj-clex  37032  bj-nul  37057  dissneqlem  37341  wl-issetft  37583  snen1g  43537  rr-spce  44217  iotaexeu  44437  elnev  44457  ax6e2nd  44578  ax6e2ndVD  44928  ax6e2ndALT  44950  upbdrech  45317  itgsubsticclem  45990