Theorem isset 3450

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem isset

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

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

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 3438

This theorem is referenced by:  issetft  3452  issetri  3455  elex  3457  elexOLD  3458  eueq  3668  ru  3740  ruOLD  3741  sbc5ALT  3771  sbccomlem  3821  snprc  4669  snssb  4734  vprc  5254  eusvnfb  5332  reusv2lem3  5339  fvmptd3f  6945  fvmptdv2  6948  ovmpodf  7505  rankf  9690  fnpr2ob  17462  isssc  17727  lrrecfr  27855  snelsingles  35896  bj-snglex  36947  bj-abex  37004  bj-clex  37005  bj-nul  37030  dissneqlem  37314  wl-issetft  37556  snen1g  43497  rr-spce  44177  iotaexeu  44391  elnev  44411  ax6e2nd  44532  ax6e2ndVD  44881  ax6e2ndALT  44903  upbdrech  45287  itgsubsticclem  45956