Theorem iotaex 6337

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 6331	. . . . 5 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑧) → (℩𝑥𝜑) = 𝑧)
2	1	eqcomd 2829	. . . 4 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑧) → 𝑧 = (℩𝑥𝜑))
3	2	eximi 1835	. . 3 ⊢ (∃𝑧∀𝑥(𝜑 ↔ 𝑥 = 𝑧) → ∃𝑧 𝑧 = (℩𝑥𝜑))
4		eu6 2659	. . 3 ⊢ (∃!𝑥𝜑 ↔ ∃𝑧∀𝑥(𝜑 ↔ 𝑥 = 𝑧))
5		isset 3508	. . 3 ⊢ ((℩𝑥𝜑) ∈ V ↔ ∃𝑧 𝑧 = (℩𝑥𝜑))
6	3, 4, 5	3imtr4i 294	. 2 ⊢ (∃!𝑥𝜑 → (℩𝑥𝜑) ∈ V)
7		iotanul 6335	. . 3 ⊢ (¬ ∃!𝑥𝜑 → (℩𝑥𝜑) = ∅)
8		0ex 5213	. . 3 ⊢ ∅ ∈ V
9	7, 8	eqeltrdi 2923	. 2 ⊢ (¬ ∃!𝑥𝜑 → (℩𝑥𝜑) ∈ V)
10	6, 9	pm2.61i 184	1 ⊢ (℩𝑥𝜑) ∈ V

Syntax hints:  ¬ wn 3   ↔ wb 208  ∀wal 1535   = wceq 1537  ∃wex 1780   ∈ wcel 2114  ∃!weu 2653  Vcvv 3496  ∅c0 4293  ℩cio 6314

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-nul 5212

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-sn 4570  df-pr 4572  df-uni 4841  df-iota 6316

This theorem is referenced by:  iota4an  6339  fvex  6685  riotaex  7120  erov  8396  iunfictbso  9542  isf32lem9  9785  sumex  15046  prodex  15263  pcval  16183  grpidval  17873  fn0g  17875  gsumvalx  17888  psgnfn  18631  psgnval  18637  dchrptlem1  25842  lgsdchrval  25932  lgsdchr  25933  bnj1366  32103  nosupno  33205  nosupdm  33206  nosupbday  33207  nosupfv  33208  nosupres  33209  nosupbnd1lem1  33210  bj-finsumval0  34569  ellimciota  41902  fourierdlem36  42435  eubrdm  43278  dfatafv2ex  43419  afv2ex  43420  funressndmafv2rn  43429