Theorem iotaex 6468

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 2146, ax-11 2162, ax-12 2184. (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 6463	. . . 4 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = 𝑦)
2		vex 3444	. . . 4 ⊢ 𝑦 ∈ V
3	1, 2	eqeltrdi 2844	. . 3 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
4	3	exlimiv 1931	. 2 ⊢ (∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
5		iotanul2 6465	. . 3 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = ∅)
6		0ex 5252	. . 3 ⊢ ∅ ∈ V
7	5, 6	eqeltrdi 2844	. 2 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
8	4, 7	pm2.61i 182	1 ⊢ (℩𝑥𝜑) ∈ V

Syntax hints:  ¬ wn 3   = wceq 1541  ∃wex 1780   ∈ wcel 2113  {cab 2714  Vcvv 3440  ∅c0 4285  {csn 4580  ℩cio 6446

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-nul 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-sn 4581  df-pr 4583  df-uni 4864  df-iota 6448

This theorem is referenced by:  iota4an  6474  fvex  6847  riotaex  7319  erov  8751  iunfictbso  10024  isf32lem9  10271  sumex  15611  prodex  15828  pcval  16772  grpidval  18586  fn0g  18588  gsumvalx  18601  psgnfn  19430  psgnval  19436  dchrptlem1  27231  lgsdchrval  27321  lgsdchr  27322  nosupno  27671  nosupdm  27672  nosupbday  27673  nosupfv  27674  nosupres  27675  nosupbnd1lem1  27676  noinfno  27686  noinfdm  27687  noinffv  27689  bnj1366  34985  bj-finsumval0  37490  preex  38665  ellimciota  45860  fourierdlem36  46387  eubrdm  47282  dfatafv2ex  47459  afv2ex  47460  funressndmafv2rn  47469