Theorem iotaex 6464

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 2182. (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 6459	. . . 4 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = 𝑦)
2		vex 3441	. . . 4 ⊢ 𝑦 ∈ V
3	1, 2	eqeltrdi 2841	. . 3 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
4	3	exlimiv 1931	. 2 ⊢ (∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
5		iotanul2 6461	. . 3 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = ∅)
6		0ex 5249	. . 3 ⊢ ∅ ∈ V
7	5, 6	eqeltrdi 2841	. 2 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
8	4, 7	pm2.61i 182	1 ⊢ (℩𝑥𝜑) ∈ V

Syntax hints:  ¬ wn 3   = wceq 1541  ∃wex 1780   ∈ wcel 2113  {cab 2711  Vcvv 3437  ∅c0 4282  {csn 4577  ℩cio 6442

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 2705  ax-nul 5248

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 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-sn 4578  df-pr 4580  df-uni 4861  df-iota 6444

This theorem is referenced by:  iota4an  6470  fvex  6843  riotaex  7315  erov  8746  iunfictbso  10014  isf32lem9  10261  sumex  15599  prodex  15816  pcval  16760  grpidval  18573  fn0g  18575  gsumvalx  18588  psgnfn  19417  psgnval  19423  dchrptlem1  27205  lgsdchrval  27295  lgsdchr  27296  nosupno  27645  nosupdm  27646  nosupbday  27647  nosupfv  27648  nosupres  27649  nosupbnd1lem1  27650  noinfno  27660  noinfdm  27661  noinffv  27663  bnj1366  34864  bj-finsumval0  37352  preex  38527  ellimciota  45741  fourierdlem36  46268  eubrdm  47163  dfatafv2ex  47340  afv2ex  47341  funressndmafv2rn  47350