Theorem iotaex 6468

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 6463	. . . 4 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = 𝑦)
2		vex 3434	. . . 4 ⊢ 𝑦 ∈ V
3	1, 2	eqeltrdi 2845	. . 3 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
4	3	exlimiv 1932	. 2 ⊢ (∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
5		iotanul2 6465	. . 3 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = ∅)
6		0ex 5242	. . 3 ⊢ ∅ ∈ V
7	5, 6	eqeltrdi 2845	. 2 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
8	4, 7	pm2.61i 182	1 ⊢ (℩𝑥𝜑) ∈ V

Syntax hints:  ¬ wn 3   = wceq 1542  ∃wex 1781   ∈ wcel 2114  {cab 2715  Vcvv 3430  ∅c0 4274  {csn 4568  ℩cio 6446

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 2709  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 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-sn 4569  df-pr 4571  df-uni 4852  df-iota 6448

This theorem is referenced by:  iota4an  6474  fvex  6847  riotaex  7321  erov  8754  iunfictbso  10027  isf32lem9  10274  sumex  15641  prodex  15861  pcval  16806  grpidval  18620  fn0g  18622  gsumvalx  18635  psgnfn  19467  psgnval  19473  dchrptlem1  27241  lgsdchrval  27331  lgsdchr  27332  nosupno  27681  nosupdm  27682  nosupbday  27683  nosupfv  27684  nosupres  27685  nosupbnd1lem1  27686  noinfno  27696  noinfdm  27697  noinffv  27699  bnj1366  34987  bj-finsumval0  37615  preex  38827  ellimciota  46062  fourierdlem36  46589  eubrdm  47496  dfatafv2ex  47673  afv2ex  47674  funressndmafv2rn  47683