Theorem iotaex 6338

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.)

Assertion

Ref	Expression
iotaex	⊢ (℩𝑥𝜑) ∈ V

Proof of Theorem iotaex

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		iotaval 6332	. . . . 5 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑧) → (℩𝑥𝜑) = 𝑧)
2	1	eqcomd 2742	. . . 4 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑧) → 𝑧 = (℩𝑥𝜑))
3	2	eximi 1842	. . 3 ⊢ (∃𝑧∀𝑥(𝜑 ↔ 𝑥 = 𝑧) → ∃𝑧 𝑧 = (℩𝑥𝜑))
4		eu6 2573	. . 3 ⊢ (∃!𝑥𝜑 ↔ ∃𝑧∀𝑥(𝜑 ↔ 𝑥 = 𝑧))
5		isset 3411	. . 3 ⊢ ((℩𝑥𝜑) ∈ V ↔ ∃𝑧 𝑧 = (℩𝑥𝜑))
6	3, 4, 5	3imtr4i 295	. 2 ⊢ (∃!𝑥𝜑 → (℩𝑥𝜑) ∈ V)
7		iotanul 6336	. . 3 ⊢ (¬ ∃!𝑥𝜑 → (℩𝑥𝜑) = ∅)
8		0ex 5185	. . 3 ⊢ ∅ ∈ V
9	7, 8	eqeltrdi 2839	. 2 ⊢ (¬ ∃!𝑥𝜑 → (℩𝑥𝜑) ∈ V)
10	6, 9	pm2.61i 185	1 ⊢ (℩𝑥𝜑) ∈ V

Syntax hints:  ¬ wn 3   ↔ wb 209  ∀wal 1541   = wceq 1543  ∃wex 1787   ∈ wcel 2112  ∃!weu 2567  Vcvv 3398  ∅c0 4223  ℩cio 6314

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-nul 5184

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-ral 3056  df-rex 3057  df-v 3400  df-sbc 3684  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-sn 4528  df-pr 4530  df-uni 4806  df-iota 6316

This theorem is referenced by:  iota4an  6340  fvex  6708  riotaex  7152  erov  8474  iunfictbso  9693  isf32lem9  9940  sumex  15216  prodex  15432  pcval  16360  grpidval  18087  fn0g  18089  gsumvalx  18102  psgnfn  18847  psgnval  18853  dchrptlem1  26099  lgsdchrval  26189  lgsdchr  26190  bnj1366  32476  nosupno  33592  nosupdm  33593  nosupbday  33594  nosupfv  33595  nosupres  33596  nosupbnd1lem1  33597  noinfno  33607  noinfdm  33608  noinffv  33610  bj-finsumval0  35140  ellimciota  42773  fourierdlem36  43302  eubrdm  44145  dfatafv2ex  44320  afv2ex  44321  funressndmafv2rn  44330