MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iotaex Structured version   Visualization version   GIF version

Theorem iotaex 6009
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.)
Assertion
Ref Expression
iotaex (℩𝑥𝜑) ∈ V

Proof of Theorem iotaex
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 iotaval 6003 . . . . 5 (∀𝑥(𝜑𝑥 = 𝑧) → (℩𝑥𝜑) = 𝑧)
21eqcomd 2777 . . . 4 (∀𝑥(𝜑𝑥 = 𝑧) → 𝑧 = (℩𝑥𝜑))
32eximi 1910 . . 3 (∃𝑧𝑥(𝜑𝑥 = 𝑧) → ∃𝑧 𝑧 = (℩𝑥𝜑))
4 df-eu 2622 . . 3 (∃!𝑥𝜑 ↔ ∃𝑧𝑥(𝜑𝑥 = 𝑧))
5 isset 3359 . . 3 ((℩𝑥𝜑) ∈ V ↔ ∃𝑧 𝑧 = (℩𝑥𝜑))
63, 4, 53imtr4i 281 . 2 (∃!𝑥𝜑 → (℩𝑥𝜑) ∈ V)
7 iotanul 6007 . . 3 (¬ ∃!𝑥𝜑 → (℩𝑥𝜑) = ∅)
8 0ex 4924 . . 3 ∅ ∈ V
97, 8syl6eqel 2858 . 2 (¬ ∃!𝑥𝜑 → (℩𝑥𝜑) ∈ V)
106, 9pm2.61i 176 1 (℩𝑥𝜑) ∈ V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wal 1629   = wceq 1631  wex 1852  wcel 2145  ∃!weu 2618  Vcvv 3351  c0 4063  cio 5990
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-nul 4923
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-sn 4317  df-pr 4319  df-uni 4575  df-iota 5992
This theorem is referenced by:  iota4an  6011  fvex  6340  riotaex  6756  erov  7995  iunfictbso  9135  isf32lem9  9383  sumex  14619  prodex  14837  pcval  15749  grpidval  17461  fn0g  17463  gsumvalx  17471  psgnfn  18121  psgnval  18127  dchrptlem1  25203  lgsdchrval  25293  lgsdchr  25294  bnj1366  31231  nosupno  32179  nosupdm  32180  nosupbday  32181  nosupfv  32182  nosupres  32183  nosupbnd1lem1  32184  bj-finsumval0  33477  ellimciota  40357  fourierdlem36  40870
  Copyright terms: Public domain W3C validator