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 2152, ax-11 2168, ax-12 2189. (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 3436	. . . 4 ⊢ 𝑦 ∈ V
3	1, 2	eqeltrdi 2848	. . 3 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
4	3	exlimiv 1937	. 2 ⊢ (∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
5		iotanul2 6465	. . 3 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = ∅)
6		0ex 5236	. . 3 ⊢ ∅ ∈ V
7	5, 6	eqeltrdi 2848	. 2 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
8	4, 7	pm2.61i 183	1 ⊢ (℩𝑥𝜑) ∈ V

Syntax hints:  ¬ wn 3   = wceq 1547  ∃wex 1786   ∈ wcel 2119  {cab 2718  Vcvv 3432  ∅c0 4268  {csn 4562  ℩cio 6446

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-nul 5235

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-sn 4563  df-pr 4565  df-uni 4846  df-iota 6448

This theorem is referenced by:  iota4an  6474  fvex  6847  riotaex  7324  erov  8758  iunfictbso  10034  isf32lem9  10281  sumex  15648  prodex  15868  pcval  16813  grpidval  18627  fn0g  18629  gsumvalx  18642  psgnfn  19474  psgnval  19480  dchrptlem1  27252  lgsdchrval  27342  lgsdchr  27343  nosupno  27692  nosupdm  27693  nosupbday  27694  nosupfv  27695  nosupres  27696  nosupbnd1lem1  27697  noinfno  27707  noinfdm  27708  noinffv  27710  bnj1366  35018  bj-finsumval0  37652  preex  38866  ellimciota  46066  fourierdlem36  46593  eubrdm  47506  dfatafv2ex  47683  afv2ex  47684  funressndmafv2rn  47693