Theorem iotaex 6513

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 2178, ax-11 2194, ax-12 2215. (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 6508	. . . 4 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = 𝑦)
2		vex 3457	. . . 4 ⊢ 𝑦 ∈ V
3	1, 2	eqeltrdi 2870	. . 3 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
4	3	exlimiv 1963	. 2 ⊢ (∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
5		iotanul2 6510	. . 3 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = ∅)
6		0ex 5268	. . 3 ⊢ ∅ ∈ V
7	5, 6	eqeltrdi 2870	. 2 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
8	4, 7	pm2.61i 184	1 ⊢ (℩𝑥𝜑) ∈ V

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1570  ∃wex 1812   ∈ wcel 2145  {cab 2740  Vcvv 3453  ∅c0 4282  {csn 4587  ℩cio 6491

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-nul 5267

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-sn 4588  df-pr 4590  df-uni 4871  df-iota 6493

This theorem is used by:  iota4an  6519  fvex  6895  riotaex  7378  erov  8818  iunfictbso  10121  isf32lem9  10367  sumex  15779  prodex  15998  pcval  16942  grpidval  18760  fn0g  18762  gsumvalx  18784  psgnfn  19634  psgnval  19640  dchrptlem1  27508  lgsdchrval  27598  lgsdchr  27599  nosupno  27947  nosupdm  27948  nosupbday  27949  nosupfv  27950  nosupres  27951  nosupbnd1lem1  27952  noinfno  27962  noinfdm  27963  noinffv  27965  bnj1366  35346  bj-finsumval0  38045  preex  39248  ellimciota  46452  fourierdlem36  46979  eubrdm  47932  dfatafv2ex  48109  afv2ex  48110  funressndmafv2rn  48119