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

Theorem iotaex 6308
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 6302 . . . . 5 (∀𝑥(𝜑𝑥 = 𝑧) → (℩𝑥𝜑) = 𝑧)
21eqcomd 2807 . . . 4 (∀𝑥(𝜑𝑥 = 𝑧) → 𝑧 = (℩𝑥𝜑))
32eximi 1836 . . 3 (∃𝑧𝑥(𝜑𝑥 = 𝑧) → ∃𝑧 𝑧 = (℩𝑥𝜑))
4 eu6 2637 . . 3 (∃!𝑥𝜑 ↔ ∃𝑧𝑥(𝜑𝑥 = 𝑧))
5 isset 3456 . . 3 ((℩𝑥𝜑) ∈ V ↔ ∃𝑧 𝑧 = (℩𝑥𝜑))
63, 4, 53imtr4i 295 . 2 (∃!𝑥𝜑 → (℩𝑥𝜑) ∈ V)
7 iotanul 6306 . . 3 (¬ ∃!𝑥𝜑 → (℩𝑥𝜑) = ∅)
8 0ex 5178 . . 3 ∅ ∈ V
97, 8eqeltrdi 2901 . 2 (¬ ∃!𝑥𝜑 → (℩𝑥𝜑) ∈ V)
106, 9pm2.61i 185 1 (℩𝑥𝜑) ∈ V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 209  wal 1536   = wceq 1538  wex 1781  wcel 2112  ∃!weu 2631  Vcvv 3444  c0 4246  cio 6285
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-nul 5177
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-ral 3114  df-rex 3115  df-v 3446  df-sbc 3724  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-sn 4529  df-pr 4531  df-uni 4804  df-iota 6287
This theorem is referenced by:  iota4an  6310  fvex  6662  riotaex  7101  erov  8381  iunfictbso  9529  isf32lem9  9776  sumex  15040  prodex  15257  pcval  16175  grpidval  17867  fn0g  17869  gsumvalx  17882  psgnfn  18625  psgnval  18631  dchrptlem1  25852  lgsdchrval  25942  lgsdchr  25943  bnj1366  32215  nosupno  33317  nosupdm  33318  nosupbday  33319  nosupfv  33320  nosupres  33321  nosupbnd1lem1  33322  bj-finsumval0  34701  ellimciota  42253  fourierdlem36  42782  eubrdm  43625  dfatafv2ex  43766  afv2ex  43767  funressndmafv2rn  43776
  Copyright terms: Public domain W3C validator