Theorem iotaex 6521

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 2130, ax-11 2147, ax-12 2167. (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 6516	. . . 4 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = 𝑦)
2		vex 3475	. . . 4 ⊢ 𝑦 ∈ V
3	1, 2	eqeltrdi 2837	. . 3 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
4	3	exlimiv 1926	. 2 ⊢ (∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
5		iotanul2 6518	. . 3 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = ∅)
6		0ex 5307	. . 3 ⊢ ∅ ∈ V
7	5, 6	eqeltrdi 2837	. 2 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
8	4, 7	pm2.61i 182	1 ⊢ (℩𝑥𝜑) ∈ V

Syntax hints:  ¬ wn 3   = wceq 1534  ∃wex 1774   ∈ wcel 2099  {cab 2705  Vcvv 3471  ∅c0 4323  {csn 4629  ℩cio 6498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-nul 5306

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2938  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-sn 4630  df-pr 4632  df-uni 4909  df-iota 6500

This theorem is referenced by:  iota4an  6530  fvex  6910  riotaex  7380  erov  8833  iunfictbso  10138  isf32lem9  10385  sumex  15667  prodex  15884  pcval  16813  grpidval  18621  fn0g  18623  gsumvalx  18636  psgnfn  19456  psgnval  19462  dchrptlem1  27210  lgsdchrval  27300  lgsdchr  27301  nosupno  27649  nosupdm  27650  nosupbday  27651  nosupfv  27652  nosupres  27653  nosupbnd1lem1  27654  noinfno  27664  noinfdm  27665  noinffv  27667  bnj1366  34460  bj-finsumval0  36764  ellimciota  45002  fourierdlem36  45531  eubrdm  46418  dfatafv2ex  46593  afv2ex  46594  funressndmafv2rn  46603