Theorem iotaex 6474

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 2147, ax-11 2163, ax-12 2185. (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 6469	. . . 4 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = 𝑦)
2		vex 3433	. . . 4 ⊢ 𝑦 ∈ V
3	1, 2	eqeltrdi 2844	. . 3 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
4	3	exlimiv 1932	. 2 ⊢ (∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
5		iotanul2 6471	. . 3 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = ∅)
6		0ex 5242	. . 3 ⊢ ∅ ∈ V
7	5, 6	eqeltrdi 2844	. 2 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
8	4, 7	pm2.61i 182	1 ⊢ (℩𝑥𝜑) ∈ V

Syntax hints:  ¬ wn 3   = wceq 1542  ∃wex 1781   ∈ wcel 2114  {cab 2714  Vcvv 3429  ∅c0 4273  {csn 4567  ℩cio 6452

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-sn 4568  df-pr 4570  df-uni 4851  df-iota 6454

This theorem is referenced by:  iota4an  6480  fvex  6853  riotaex  7328  erov  8761  iunfictbso  10036  isf32lem9  10283  sumex  15650  prodex  15870  pcval  16815  grpidval  18629  fn0g  18631  gsumvalx  18644  psgnfn  19476  psgnval  19482  dchrptlem1  27227  lgsdchrval  27317  lgsdchr  27318  nosupno  27667  nosupdm  27668  nosupbday  27669  nosupfv  27670  nosupres  27671  nosupbnd1lem1  27672  noinfno  27682  noinfdm  27683  noinffv  27685  bnj1366  34971  bj-finsumval0  37599  preex  38813  ellimciota  46044  fourierdlem36  46571  eubrdm  47484  dfatafv2ex  47661  afv2ex  47662  funressndmafv2rn  47671