Theorem isset 3445

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem isset

Step	Hyp	Ref	Expression
1		dfclel 2817	. 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V))
2		vex 3436	. . . 4 ⊢ 𝑥 ∈ V
3	2	biantru 530	. . 3 ⊢ (𝑥 = 𝐴 ↔ (𝑥 = 𝐴 ∧ 𝑥 ∈ V))
4	3	exbii 1850	. 2 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V))
5	1, 4	bitr4i 277	1 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)

Syntax hints:   ↔ wb 205   ∧ wa 396   = wceq 1539  ∃wex 1782   ∈ wcel 2106  Vcvv 3432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434

This theorem is referenced by:  issetf  3446  issetri  3448  elex  3450  eueq  3643  ru  3715  sbc5ALT  3745  snprc  4653  vprc  5239  eusvnfb  5316  reusv2lem3  5323  iotaex  6413  funimaexg  6520  fvmptd3f  6890  fvmptdv2  6893  ovmpodf  7429  rankf  9552  fnpr2ob  17269  isssc  17532  lrrecfr  34100  snelsingles  34224  bj-snglex  35163  bj-nul  35227  dissneqlem  35511  snen1g  41131  rr-spce  41815  iotaexeu  42036  elnev  42056  ax6e2nd  42178  ax6e2ndVD  42528  ax6e2ndALT  42550  upbdrech  42844  itgsubsticclem  43516