Theorem iotaex 6546

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 2141, ax-11 2158, ax-12 2178. (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 6541	. . . 4 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = 𝑦)
2		vex 3492	. . . 4 ⊢ 𝑦 ∈ V
3	1, 2	eqeltrdi 2852	. . 3 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
4	3	exlimiv 1929	. 2 ⊢ (∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
5		iotanul2 6543	. . 3 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = ∅)
6		0ex 5325	. . 3 ⊢ ∅ ∈ V
7	5, 6	eqeltrdi 2852	. 2 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
8	4, 7	pm2.61i 182	1 ⊢ (℩𝑥𝜑) ∈ V

Syntax hints:  ¬ wn 3   = wceq 1537  ∃wex 1777   ∈ wcel 2108  {cab 2717  Vcvv 3488  ∅c0 4352  {csn 4648  ℩cio 6523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-nul 5324

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-sn 4649  df-pr 4651  df-uni 4932  df-iota 6525

This theorem is referenced by:  iota4an  6555  fvex  6933  riotaex  7408  erov  8872  iunfictbso  10183  isf32lem9  10430  sumex  15736  prodex  15953  pcval  16891  grpidval  18699  fn0g  18701  gsumvalx  18714  psgnfn  19543  psgnval  19549  dchrptlem1  27326  lgsdchrval  27416  lgsdchr  27417  nosupno  27766  nosupdm  27767  nosupbday  27768  nosupfv  27769  nosupres  27770  nosupbnd1lem1  27771  noinfno  27781  noinfdm  27782  noinffv  27784  bnj1366  34805  bj-finsumval0  37251  ellimciota  45535  fourierdlem36  46064  eubrdm  46951  dfatafv2ex  47128  afv2ex  47129  funressndmafv2rn  47138