Theorem isset 3467

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem isset

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

Syntax hints:   ↔ wb 208   = wceq 1559  ∃wex 1798   ∈ wcel 2141  Vcvv 3453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455

This theorem is referenced by:  issetft  3469  issetri  3472  elex  3474  eueq  3669  ru  3741  sbc5ALT  3771  sbccomlem  3820  snprc  4673  snssb  4738  vprcOLD  5268  eusvnfb  5347  reusv2lem3  5354  fvmptd3f  6986  fvmptdv2  6989  ovmpodf  7547  rankf  9746  fnpr2ob  17579  isssc  17844  lrrecfr  28024  snelsingles  36231  bj-sbcex  37084  bj-snglex  37419  bj-abex  37476  bj-clex  37477  bj-nul  37502  dissneqlem  37795  wl-issetft  38046  snen1g  44061  rr-spce  44741  iotaexeu  44955  elnev  44974  ax6e2nd  45095  ax6e2ndVD  45444  ax6e2ndALT  45466  upbdrech  45845  itgsubsticclem  46510