Theorem iotaex 6515

Description: Theorem 8.23 in [Quine] p. 58. This theorem proves the existence of the ℩ class under our definition. (Contributed by Andrew Salmon, 11-Jul-2011.) Remove dependency on ax-10 2135, ax-11 2152, ax-12 2169. (Revised by SN, 6-Nov-2024.)

Assertion

Ref	Expression
iotaex	⊢ (℩𝑥𝜑) ∈ V

Proof of Theorem iotaex

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		iotaval2 6510	. . . 4 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = 𝑦)
2		vex 3476	. . . 4 ⊢ 𝑦 ∈ V
3	1, 2	eqeltrdi 2839	. . 3 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
4	3	exlimiv 1931	. 2 ⊢ (∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
5		iotanul2 6512	. . 3 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = ∅)
6		0ex 5306	. . 3 ⊢ ∅ ∈ V
7	5, 6	eqeltrdi 2839	. 2 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
8	4, 7	pm2.61i 182	1 ⊢ (℩𝑥𝜑) ∈ V

Syntax hints:  ¬ wn 3   = wceq 1539  ∃wex 1779   ∈ wcel 2104  {cab 2707  Vcvv 3472  ∅c0 4321  {csn 4627  ℩cio 6492

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-nul 5305

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-sn 4628  df-pr 4630  df-uni 4908  df-iota 6494

This theorem is referenced by:  iota4an  6524  fvex  6903  riotaex  7371  erov  8810  iunfictbso  10111  isf32lem9  10358  sumex  15638  prodex  15855  pcval  16781  grpidval  18586  fn0g  18588  gsumvalx  18601  psgnfn  19410  psgnval  19416  dchrptlem1  27003  lgsdchrval  27093  lgsdchr  27094  nosupno  27442  nosupdm  27443  nosupbday  27444  nosupfv  27445  nosupres  27446  nosupbnd1lem1  27447  noinfno  27457  noinfdm  27458  noinffv  27460  bnj1366  34138  bj-finsumval0  36469  ellimciota  44628  fourierdlem36  45157  eubrdm  46044  dfatafv2ex  46219  afv2ex  46220  funressndmafv2rn  46229