Theorem iotaex 6519

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 2179, ax-11 2195, ax-12 2216. (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 6514	. . . 4 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = 𝑦)
2		vex 3462	. . . 4 ⊢ 𝑦 ∈ V
3	1, 2	eqeltrdi 2874	. . 3 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
4	3	exlimiv 1963	. 2 ⊢ (∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
5		iotanul2 6516	. . 3 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = ∅)
6		0ex 5275	. . 3 ⊢ ∅ ∈ V
7	5, 6	eqeltrdi 2874	. 2 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
8	4, 7	pm2.61i 184	1 ⊢ (℩𝑥𝜑) ∈ V

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1570  ∃wex 1812   ∈ wcel 2146  {cab 2744  Vcvv 3458  ∅c0 4289  {csn 4594  ℩cio 6497

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 2148  ax-9 2156  ax-ext 2738  ax-nul 5274

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 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-sn 4595  df-pr 4597  df-uni 4878  df-iota 6499

This theorem is used by:  iota4an  6525  fvex  6901  riotaex  7384  erov  8821  iunfictbso  10117  isf32lem9  10363  sumex  15765  prodex  15985  pcval  16929  grpidval  18744  fn0g  18746  gsumvalx  18763  psgnfn  19602  psgnval  19608  dchrptlem1  27465  lgsdchrval  27555  lgsdchr  27556  nosupno  27904  nosupdm  27905  nosupbday  27906  nosupfv  27907  nosupres  27908  nosupbnd1lem1  27909  noinfno  27919  noinfdm  27920  noinffv  27922  bnj1366  35249  bj-finsumval0  37970  preex  39182  ellimciota  46371  fourierdlem36  46898  eubrdm  47814  dfatafv2ex  47991  afv2ex  47992  funressndmafv2rn  48001