Theorem iotaex 6491

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 2174, ax-11 2190, ax-12 2211. (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 6486	. . . 4 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = 𝑦)
2		vex 3457	. . . 4 ⊢ 𝑦 ∈ V
3	1, 2	eqeltrdi 2869	. . 3 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
4	3	exlimiv 1949	. 2 ⊢ (∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
5		iotanul2 6488	. . 3 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = ∅)
6		0ex 5254	. . 3 ⊢ ∅ ∈ V
7	5, 6	eqeltrdi 2869	. 2 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
8	4, 7	pm2.61i 183	1 ⊢ (℩𝑥𝜑) ∈ V

Syntax hints:  ¬ wn 3   = wceq 1559  ∃wex 1798   ∈ wcel 2141  {cab 2739  Vcvv 3453  ∅c0 4283  {csn 4579  ℩cio 6469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-nul 5253

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-sn 4580  df-pr 4582  df-uni 4863  df-iota 6471

This theorem is referenced by:  iota4an  6497  fvex  6874  riotaex  7351  erov  8789  iunfictbso  10063  isf32lem9  10311  sumex  15705  prodex  15925  pcval  16870  grpidval  18685  fn0g  18687  gsumvalx  18700  psgnfn  19531  psgnval  19537  dchrptlem1  27315  lgsdchrval  27405  lgsdchr  27406  nosupno  27754  nosupdm  27755  nosupbday  27756  nosupfv  27757  nosupres  27758  nosupbnd1lem1  27759  noinfno  27769  noinfdm  27770  noinffv  27772  bnj1366  35084  bj-finsumval0  37737  preex  38951  ellimciota  46150  fourierdlem36  46677  eubrdm  47590  dfatafv2ex  47767  afv2ex  47768  funressndmafv2rn  47777