Theorem iotaex 6509

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 6504	. . . 4 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = 𝑦)
2		vex 3468	. . . 4 ⊢ 𝑦 ∈ V
3	1, 2	eqeltrdi 2843	. . 3 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
4	3	exlimiv 1930	. 2 ⊢ (∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
5		iotanul2 6506	. . 3 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = ∅)
6		0ex 5282	. . 3 ⊢ ∅ ∈ V
7	5, 6	eqeltrdi 2843	. 2 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
8	4, 7	pm2.61i 182	1 ⊢ (℩𝑥𝜑) ∈ V

Syntax hints:  ¬ wn 3   = wceq 1540  ∃wex 1779   ∈ wcel 2109  {cab 2714  Vcvv 3464  ∅c0 4313  {csn 4606  ℩cio 6487

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 2708  ax-nul 5281

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 2715  df-cleq 2728  df-clel 2810  df-ne 2934  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-sn 4607  df-pr 4609  df-uni 4889  df-iota 6489

This theorem is referenced by:  iota4an  6518  fvex  6894  riotaex  7371  erov  8833  iunfictbso  10133  isf32lem9  10380  sumex  15709  prodex  15926  pcval  16869  grpidval  18644  fn0g  18646  gsumvalx  18659  psgnfn  19487  psgnval  19493  dchrptlem1  27232  lgsdchrval  27322  lgsdchr  27323  nosupno  27672  nosupdm  27673  nosupbday  27674  nosupfv  27675  nosupres  27676  nosupbnd1lem1  27677  noinfno  27687  noinfdm  27688  noinffv  27690  bnj1366  34865  bj-finsumval0  37308  ellimciota  45610  fourierdlem36  46139  eubrdm  47032  dfatafv2ex  47209  afv2ex  47210  funressndmafv2rn  47219