Theorem iotaex 6462

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 2142, ax-11 2158, ax-12 2178. (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 6457	. . . 4 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = 𝑦)
2		vex 3442	. . . 4 ⊢ 𝑦 ∈ V
3	1, 2	eqeltrdi 2836	. . 3 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
4	3	exlimiv 1930	. 2 ⊢ (∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
5		iotanul2 6459	. . 3 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = ∅)
6		0ex 5249	. . 3 ⊢ ∅ ∈ V
7	5, 6	eqeltrdi 2836	. 2 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
8	4, 7	pm2.61i 182	1 ⊢ (℩𝑥𝜑) ∈ V

Syntax hints:  ¬ wn 3   = wceq 1540  ∃wex 1779   ∈ wcel 2109  {cab 2707  Vcvv 3438  ∅c0 4286  {csn 4579  ℩cio 6440

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5248

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-sn 4580  df-pr 4582  df-uni 4862  df-iota 6442

This theorem is referenced by:  iota4an  6468  fvex  6839  riotaex  7314  erov  8748  iunfictbso  10027  isf32lem9  10274  sumex  15613  prodex  15830  pcval  16774  grpidval  18553  fn0g  18555  gsumvalx  18568  psgnfn  19398  psgnval  19404  dchrptlem1  27191  lgsdchrval  27281  lgsdchr  27282  nosupno  27631  nosupdm  27632  nosupbday  27633  nosupfv  27634  nosupres  27635  nosupbnd1lem1  27636  noinfno  27646  noinfdm  27647  noinffv  27649  bnj1366  34795  bj-finsumval0  37258  ellimciota  45596  fourierdlem36  46125  eubrdm  47021  dfatafv2ex  47198  afv2ex  47199  funressndmafv2rn  47208