Theorem iotaex 6206

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 6200	. . . . 5 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑧) → (℩𝑥𝜑) = 𝑧)
2	1	eqcomd 2801	. . . 4 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑧) → 𝑧 = (℩𝑥𝜑))
3	2	eximi 1816	. . 3 ⊢ (∃𝑧∀𝑥(𝜑 ↔ 𝑥 = 𝑧) → ∃𝑧 𝑧 = (℩𝑥𝜑))
4		eu6 2617	. . 3 ⊢ (∃!𝑥𝜑 ↔ ∃𝑧∀𝑥(𝜑 ↔ 𝑥 = 𝑧))
5		isset 3449	. . 3 ⊢ ((℩𝑥𝜑) ∈ V ↔ ∃𝑧 𝑧 = (℩𝑥𝜑))
6	3, 4, 5	3imtr4i 293	. 2 ⊢ (∃!𝑥𝜑 → (℩𝑥𝜑) ∈ V)
7		iotanul 6204	. . 3 ⊢ (¬ ∃!𝑥𝜑 → (℩𝑥𝜑) = ∅)
8		0ex 5102	. . 3 ⊢ ∅ ∈ V
9	7, 8	syl6eqel 2891	. 2 ⊢ (¬ ∃!𝑥𝜑 → (℩𝑥𝜑) ∈ V)
10	6, 9	pm2.61i 183	1 ⊢ (℩𝑥𝜑) ∈ V

Syntax hints:  ¬ wn 3   ↔ wb 207  ∀wal 1520   = wceq 1522  ∃wex 1761   ∈ wcel 2081  ∃!weu 2611  Vcvv 3437  ∅c0 4211  ℩cio 6187

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769  ax-nul 5101

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-rex 3111  df-v 3439  df-sbc 3707  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-sn 4473  df-pr 4475  df-uni 4746  df-iota 6189

This theorem is referenced by:  iota4an  6208  fvex  6551  riotaex  6981  erov  8244  iunfictbso  9386  isf32lem9  9629  sumex  14878  prodex  15094  pcval  16010  grpidval  17699  fn0g  17701  gsumvalx  17709  psgnfn  18360  psgnval  18366  dchrptlem1  25522  lgsdchrval  25612  lgsdchr  25613  bnj1366  31718  nosupno  32812  nosupdm  32813  nosupbday  32814  nosupfv  32815  nosupres  32816  nosupbnd1lem1  32817  bj-finsumval0  34119  ellimciota  41437  fourierdlem36  41970  eubrdm  42787  dfatafv2ex  42928  afv2ex  42929  funressndmafv2rn  42938