Theorem iotaex 6513

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 2138, ax-11 2155, ax-12 2172. (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 6508	. . . 4 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = 𝑦)
2		vex 3479	. . . 4 ⊢ 𝑦 ∈ V
3	1, 2	eqeltrdi 2842	. . 3 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
4	3	exlimiv 1934	. 2 ⊢ (∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
5		iotanul2 6510	. . 3 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = ∅)
6		0ex 5306	. . 3 ⊢ ∅ ∈ V
7	5, 6	eqeltrdi 2842	. 2 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
8	4, 7	pm2.61i 182	1 ⊢ (℩𝑥𝜑) ∈ V

Syntax hints:  ¬ wn 3   = wceq 1542  ∃wex 1782   ∈ wcel 2107  {cab 2710  Vcvv 3475  ∅c0 4321  {csn 4627  ℩cio 6490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-nul 5305

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-v 3477  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-sn 4628  df-pr 4630  df-uni 4908  df-iota 6492

This theorem is referenced by:  iota4an  6522  fvex  6901  riotaex  7364  erov  8804  iunfictbso  10105  isf32lem9  10352  sumex  15630  prodex  15847  pcval  16773  grpidval  18576  fn0g  18578  gsumvalx  18591  psgnfn  19362  psgnval  19368  dchrptlem1  26747  lgsdchrval  26837  lgsdchr  26838  nosupno  27186  nosupdm  27187  nosupbday  27188  nosupfv  27189  nosupres  27190  nosupbnd1lem1  27191  noinfno  27201  noinfdm  27202  noinffv  27204  bnj1366  33778  bj-finsumval0  36104  ellimciota  44265  fourierdlem36  44794  eubrdm  45681  dfatafv2ex  45856  afv2ex  45857  funressndmafv2rn  45866