Theorem iotaex 6533

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 2140, ax-11 2156, ax-12 2176. (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 6528	. . . 4 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = 𝑦)
2		vex 3483	. . . 4 ⊢ 𝑦 ∈ V
3	1, 2	eqeltrdi 2848	. . 3 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
4	3	exlimiv 1929	. 2 ⊢ (∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
5		iotanul2 6530	. . 3 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = ∅)
6		0ex 5306	. . 3 ⊢ ∅ ∈ V
7	5, 6	eqeltrdi 2848	. 2 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
8	4, 7	pm2.61i 182	1 ⊢ (℩𝑥𝜑) ∈ V

Syntax hints:  ¬ wn 3   = wceq 1539  ∃wex 1778   ∈ wcel 2107  {cab 2713  Vcvv 3479  ∅c0 4332  {csn 4625  ℩cio 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707  ax-nul 5305

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ne 2940  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-sn 4626  df-pr 4628  df-uni 4907  df-iota 6513

This theorem is referenced by:  iota4an  6542  fvex  6918  riotaex  7393  erov  8855  iunfictbso  10155  isf32lem9  10402  sumex  15725  prodex  15942  pcval  16883  grpidval  18675  fn0g  18677  gsumvalx  18690  psgnfn  19520  psgnval  19526  dchrptlem1  27309  lgsdchrval  27399  lgsdchr  27400  nosupno  27749  nosupdm  27750  nosupbday  27751  nosupfv  27752  nosupres  27753  nosupbnd1lem1  27754  noinfno  27764  noinfdm  27765  noinffv  27767  bnj1366  34844  bj-finsumval0  37287  ellimciota  45634  fourierdlem36  46163  eubrdm  47053  dfatafv2ex  47230  afv2ex  47231  funressndmafv2rn  47240