Theorem iotaex 6517

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 6512	. . . 4 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = 𝑦)
2		vex 3479	. . . 4 ⊢ 𝑦 ∈ V
3	1, 2	eqeltrdi 2842	. . 3 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
4	3	exlimiv 1934	. 2 ⊢ (∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
5		iotanul2 6514	. . 3 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = ∅)
6		0ex 5308	. . 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 4323  {csn 4629  ℩cio 6494

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 5307

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 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-sn 4630  df-pr 4632  df-uni 4910  df-iota 6496

This theorem is referenced by:  iota4an  6526  fvex  6905  riotaex  7369  erov  8808  iunfictbso  10109  isf32lem9  10356  sumex  15634  prodex  15851  pcval  16777  grpidval  18580  fn0g  18582  gsumvalx  18595  psgnfn  19369  psgnval  19375  dchrptlem1  26767  lgsdchrval  26857  lgsdchr  26858  nosupno  27206  nosupdm  27207  nosupbday  27208  nosupfv  27209  nosupres  27210  nosupbnd1lem1  27211  noinfno  27221  noinfdm  27222  noinffv  27224  bnj1366  33840  bj-finsumval0  36166  ellimciota  44330  fourierdlem36  44859  eubrdm  45746  dfatafv2ex  45921  afv2ex  45922  funressndmafv2rn  45931