Theorem iotaex 6476

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 6471	. . . 4 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = 𝑦)
2		vex 3446	. . . 4 ⊢ 𝑦 ∈ V
3	1, 2	eqeltrdi 2845	. . 3 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
4	3	exlimiv 1932	. 2 ⊢ (∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
5		iotanul2 6473	. . 3 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = ∅)
6		0ex 5254	. . 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 6454

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 5253

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 6456

This theorem is referenced by:  iota4an  6482  fvex  6855  riotaex  7329  erov  8763  iunfictbso  10036  isf32lem9  10283  sumex  15623  prodex  15840  pcval  16784  grpidval  18598  fn0g  18600  gsumvalx  18613  psgnfn  19442  psgnval  19448  dchrptlem1  27243  lgsdchrval  27333  lgsdchr  27334  nosupno  27683  nosupdm  27684  nosupbday  27685  nosupfv  27686  nosupres  27687  nosupbnd1lem1  27688  noinfno  27698  noinfdm  27699  noinffv  27701  bnj1366  35004  bj-finsumval0  37537  preex  38740  ellimciota  45971  fourierdlem36  46498  eubrdm  47393  dfatafv2ex  47570  afv2ex  47571  funressndmafv2rn  47580