Theorem iotaex 6484

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 2142, ax-11 2158, ax-12 2178. (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 6479	. . . 4 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = 𝑦)
2		vex 3451	. . . 4 ⊢ 𝑦 ∈ V
3	1, 2	eqeltrdi 2836	. . 3 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
4	3	exlimiv 1930	. 2 ⊢ (∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
5		iotanul2 6481	. . 3 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = ∅)
6		0ex 5262	. . 3 ⊢ ∅ ∈ V
7	5, 6	eqeltrdi 2836	. 2 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
8	4, 7	pm2.61i 182	1 ⊢ (℩𝑥𝜑) ∈ V

Syntax hints:  ¬ wn 3   = wceq 1540  ∃wex 1779   ∈ wcel 2109  {cab 2707  Vcvv 3447  ∅c0 4296  {csn 4589  ℩cio 6462

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5261

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-sn 4590  df-pr 4592  df-uni 4872  df-iota 6464

This theorem is referenced by:  iota4an  6493  fvex  6871  riotaex  7348  erov  8787  iunfictbso  10067  isf32lem9  10314  sumex  15654  prodex  15871  pcval  16815  grpidval  18588  fn0g  18590  gsumvalx  18603  psgnfn  19431  psgnval  19437  dchrptlem1  27175  lgsdchrval  27265  lgsdchr  27266  nosupno  27615  nosupdm  27616  nosupbday  27617  nosupfv  27618  nosupres  27619  nosupbnd1lem1  27620  noinfno  27630  noinfdm  27631  noinffv  27633  bnj1366  34819  bj-finsumval0  37273  ellimciota  45612  fourierdlem36  46141  eubrdm  47034  dfatafv2ex  47211  afv2ex  47212  funressndmafv2rn  47221