Theorem iotaex 6478

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 6473	. . . 4 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = 𝑦)
2		vex 3446	. . . 4 ⊢ 𝑦 ∈ V
3	1, 2	eqeltrdi 2845	. . 3 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
4	3	exlimiv 1932	. 2 ⊢ (∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
5		iotanul2 6475	. . 3 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = ∅)
6		0ex 5256	. . 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 3442  ∅c0 4287  {csn 4582  ℩cio 6456

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 5255

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 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-sn 4583  df-pr 4585  df-uni 4866  df-iota 6458

This theorem is referenced by:  iota4an  6484  fvex  6857  riotaex  7331  erov  8765  iunfictbso  10038  isf32lem9  10285  sumex  15625  prodex  15842  pcval  16786  grpidval  18600  fn0g  18602  gsumvalx  18615  psgnfn  19447  psgnval  19453  dchrptlem1  27248  lgsdchrval  27338  lgsdchr  27339  nosupno  27688  nosupdm  27689  nosupbday  27690  nosupfv  27691  nosupres  27692  nosupbnd1lem1  27693  noinfno  27703  noinfdm  27704  noinffv  27706  bnj1366  35011  bj-finsumval0  37567  preex  38772  ellimciota  46003  fourierdlem36  46530  eubrdm  47425  dfatafv2ex  47602  afv2ex  47603  funressndmafv2rn  47612