Theorem iotaex 6507

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 2213. (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 6502	. . . 4 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = 𝑦)
2		vex 3455	. . . 4 ⊢ 𝑦 ∈ V
3	1, 2	eqeltrdi 2869	. . 3 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
4	3	exlimiv 1963	. 2 ⊢ (∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
5		iotanul2 6504	. . 3 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = ∅)
6		0ex 5261	. . 3 ⊢ ∅ ∈ V
7	5, 6	eqeltrdi 2869	. 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 2739  Vcvv 3451  ∅c0 4279  {csn 4584  ℩cio 6485

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 2733  ax-nul 5260

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 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-sn 4585  df-pr 4587  df-uni 4868  df-iota 6487

This theorem is used by:  iota4an  6513  fvex  6890  riotaex  7373  erov  8819  iunfictbso  10174  isf32lem9  10420  sumex  15835  prodex  16054  pcval  17002  grpidval  18820  fn0g  18823  gsumvalx  18845  psgnfn  19695  psgnval  19701  dchrptlem1  27573  lgsdchrval  27663  lgsdchr  27664  nosupno  28042  nosupdm  28043  nosupbday  28044  nosupfv  28045  nosupres  28046  nosupbnd1lem1  28047  noinfno  28057  noinfdm  28058  noinffv  28060  bnj1366  35442  bj-finsumval0  38174  preex  39392  ellimciota  46570  fourierdlem36  47097  eubrdm  48050  dfatafv2ex  48227  afv2ex  48228  funressndmafv2rn  48237