Theorem isset 3435

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem isset

Step	Hyp	Ref	Expression
1		dfclel 2818	. 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V))
2		vex 3426	. . . 4 ⊢ 𝑥 ∈ V
3	2	biantru 529	. . 3 ⊢ (𝑥 = 𝐴 ↔ (𝑥 = 𝐴 ∧ 𝑥 ∈ V))
4	3	exbii 1851	. 2 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V))
5	1, 4	bitr4i 277	1 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)

Syntax hints:   ↔ wb 205   ∧ wa 395   = wceq 1539  ∃wex 1783   ∈ wcel 2108  Vcvv 3422

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424

This theorem is referenced by:  issetf  3436  issetri  3438  elex  3440  eueq  3638  ru  3710  sbc5ALT  3740  snprc  4650  vprc  5234  eusvnfb  5311  reusv2lem3  5318  iotaex  6398  funimaexg  6504  fvmptd3f  6872  fvmptdv2  6875  ovmpodf  7407  rankf  9483  fnpr2ob  17186  isssc  17449  lrrecfr  34027  snelsingles  34151  bj-snglex  35090  bj-nul  35154  dissneqlem  35438  snen1g  41029  rr-spce  41704  iotaexeu  41925  elnev  41945  ax6e2nd  42067  ax6e2ndVD  42417  ax6e2ndALT  42439  upbdrech  42734  itgsubsticclem  43406