Theorem isset 3461

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem isset

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

Syntax hints:   ↔ wb 206   = wceq 1540  ∃wex 1779   ∈ wcel 2109  Vcvv 3447

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449

This theorem is referenced by:  issetft  3463  issetri  3466  elex  3468  elexOLD  3469  eueq  3679  ru  3751  ruOLD  3752  sbc5ALT  3782  sbccomlem  3832  snprc  4681  snssb  4746  vprc  5270  eusvnfb  5348  reusv2lem3  5355  iotaexOLD  6491  funimaexgOLD  6604  fvmptd3f  6983  fvmptdv2  6986  ovmpodf  7545  rankf  9747  fnpr2ob  17521  isssc  17782  lrrecfr  27850  snelsingles  35910  bj-snglex  36961  bj-abex  37018  bj-clex  37019  bj-nul  37044  dissneqlem  37328  wl-issetft  37570  snen1g  43513  rr-spce  44193  iotaexeu  44407  elnev  44427  ax6e2nd  44548  ax6e2ndVD  44897  ax6e2ndALT  44919  upbdrech  45303  itgsubsticclem  45973