Theorem iotaex 6009

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 6003	. . . . 5 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑧) → (℩𝑥𝜑) = 𝑧)
2	1	eqcomd 2777	. . . 4 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑧) → 𝑧 = (℩𝑥𝜑))
3	2	eximi 1910	. . 3 ⊢ (∃𝑧∀𝑥(𝜑 ↔ 𝑥 = 𝑧) → ∃𝑧 𝑧 = (℩𝑥𝜑))
4		df-eu 2622	. . 3 ⊢ (∃!𝑥𝜑 ↔ ∃𝑧∀𝑥(𝜑 ↔ 𝑥 = 𝑧))
5		isset 3359	. . 3 ⊢ ((℩𝑥𝜑) ∈ V ↔ ∃𝑧 𝑧 = (℩𝑥𝜑))
6	3, 4, 5	3imtr4i 281	. 2 ⊢ (∃!𝑥𝜑 → (℩𝑥𝜑) ∈ V)
7		iotanul 6007	. . 3 ⊢ (¬ ∃!𝑥𝜑 → (℩𝑥𝜑) = ∅)
8		0ex 4924	. . 3 ⊢ ∅ ∈ V
9	7, 8	syl6eqel 2858	. 2 ⊢ (¬ ∃!𝑥𝜑 → (℩𝑥𝜑) ∈ V)
10	6, 9	pm2.61i 176	1 ⊢ (℩𝑥𝜑) ∈ V

Syntax hints:  ¬ wn 3   ↔ wb 196  ∀wal 1629   = wceq 1631  ∃wex 1852   ∈ wcel 2145  ∃!weu 2618  Vcvv 3351  ∅c0 4063  ℩cio 5990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-nul 4923

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-sn 4317  df-pr 4319  df-uni 4575  df-iota 5992

This theorem is referenced by:  iota4an  6011  fvex  6340  riotaex  6756  erov  7995  iunfictbso  9135  isf32lem9  9383  sumex  14619  prodex  14837  pcval  15749  grpidval  17461  fn0g  17463  gsumvalx  17471  psgnfn  18121  psgnval  18127  dchrptlem1  25203  lgsdchrval  25293  lgsdchr  25294  bnj1366  31231  nosupno  32179  nosupdm  32180  nosupbday  32181  nosupfv  32182  nosupres  32183  nosupbnd1lem1  32184  bj-finsumval0  33477  ellimciota  40357  fourierdlem36  40870