Theorem iotaex 6514

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 2177, ax-11 2193, ax-12 2212. (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 6509	. . . 4 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = 𝑦)
2		vex 3454	. . . 4 ⊢ 𝑦 ∈ V
3	1, 2	eqeltrdi 2868	. . 3 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
4	3	exlimiv 1962	. 2 ⊢ (∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
5		iotanul2 6511	. . 3 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = ∅)
6		0ex 5260	. . 3 ⊢ ∅ ∈ V
7	5, 6	eqeltrdi 2868	. 2 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
8	4, 7	pm2.61i 184	1 ⊢ (℩𝑥𝜑) ∈ V

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1569  ∃wex 1811   ∈ wcel 2144  {cab 2738  Vcvv 3450  ∅c0 4278  {csn 4584  ℩cio 6492

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-sn 4585  df-pr 4587  df-uni 4867  df-iota 6494

This theorem is used by:  iota4an  6520  iotan0  6528  fvex  6899  riotaex  7382  erov  8839  iunfictbso  10197  isf32lem9  10443  sumex  15861  prodex  16080  pcval  17028  grpidval  18846  fn0g  18849  gsumvalx  18871  psgnfn  19721  psgnval  19727  dchrptlem1  27597  lgsdchrval  27687  lgsdchr  27688  nosupno  28066  nosupdm  28067  nosupbday  28068  nosupfv  28069  nosupres  28070  nosupbnd1lem1  28071  noinfno  28081  noinfdm  28082  noinffv  28084  bnj1366  35506  bj-finsumval0  38300  preex  39518  ellimciota  46720  fourierdlem36  47247  eubrdm  48200  dfatafv2ex  48377  afv2ex  48378  funressndmafv2rn  48387