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 4583  ℩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-dif 3899  df-un 3901  df-ss 3914  df-nul 4279  df-sn 4584  df-pr 4586  df-uni 4867  df-iota 6494

This theorem is used by:  iota4an  6520  fvex  6898  riotaex  7381  erov  8835  iunfictbso  10193  isf32lem9  10439  sumex  15855  prodex  16074  pcval  17022  grpidval  18840  fn0g  18843  gsumvalx  18865  psgnfn  19715  psgnval  19721  dchrptlem1  27591  lgsdchrval  27681  lgsdchr  27682  nosupno  28060  nosupdm  28061  nosupbday  28062  nosupfv  28063  nosupres  28064  nosupbnd1lem1  28065  noinfno  28075  noinfdm  28076  noinffv  28078  bnj1366  35459  bj-finsumval0  38207  preex  39425  ellimciota  46626  fourierdlem36  47153  eubrdm  48106  dfatafv2ex  48283  afv2ex  48284  funressndmafv2rn  48293