Theorem isset 3491

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem isset

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

Syntax hints:   ↔ wb 206   = wceq 1536  ∃wex 1775   ∈ wcel 2105  Vcvv 3477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479

This theorem is referenced by:  issetft  3493  issetri  3496  elex  3498  elexOLD  3499  eueq  3716  ru  3788  ruOLD  3789  sbc5ALT  3819  sbccomlem  3877  snprc  4721  snssb  4786  vprc  5320  eusvnfb  5398  reusv2lem3  5405  iotaexOLD  6542  funimaexgOLD  6654  fvmptd3f  7030  fvmptdv2  7033  ovmpodf  7588  rankf  9831  fnpr2ob  17604  isssc  17867  lrrecfr  27990  snelsingles  35903  bj-snglex  36955  bj-abex  37012  bj-clex  37013  bj-nul  37038  dissneqlem  37322  wl-issetft  37562  snen1g  43513  rr-spce  44193  iotaexeu  44413  elnev  44433  ax6e2nd  44555  ax6e2ndVD  44905  ax6e2ndALT  44927  upbdrech  45255  itgsubsticclem  45930