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

Theorem iotaex 6011
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 6005 . . . . 5 (∀𝑥(𝜑𝑥 = 𝑧) → (℩𝑥𝜑) = 𝑧)
21eqcomd 2776 . . . 4 (∀𝑥(𝜑𝑥 = 𝑧) → 𝑧 = (℩𝑥𝜑))
32eximi 1909 . . 3 (∃𝑧𝑥(𝜑𝑥 = 𝑧) → ∃𝑧 𝑧 = (℩𝑥𝜑))
4 df-eu 2621 . . 3 (∃!𝑥𝜑 ↔ ∃𝑧𝑥(𝜑𝑥 = 𝑧))
5 isset 3356 . . 3 ((℩𝑥𝜑) ∈ V ↔ ∃𝑧 𝑧 = (℩𝑥𝜑))
63, 4, 53imtr4i 281 . 2 (∃!𝑥𝜑 → (℩𝑥𝜑) ∈ V)
7 iotanul 6009 . . 3 (¬ ∃!𝑥𝜑 → (℩𝑥𝜑) = ∅)
8 0ex 4921 . . 3 ∅ ∈ V
97, 8syl6eqel 2857 . 2 (¬ ∃!𝑥𝜑 → (℩𝑥𝜑) ∈ V)
106, 9pm2.61i 176 1 (℩𝑥𝜑) ∈ V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wal 1628   = wceq 1630  wex 1851  wcel 2144  ∃!weu 2617  Vcvv 3349  c0 4061  cio 5992
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-nul 4920
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ral 3065  df-rex 3066  df-v 3351  df-sbc 3586  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-sn 4315  df-pr 4317  df-uni 4573  df-iota 5994
This theorem is referenced by:  iota4an  6013  fvex  6342  riotaex  6757  erov  7996  iunfictbso  9136  isf32lem9  9384  sumex  14625  prodex  14843  pcval  15755  grpidval  17467  fn0g  17469  gsumvalx  17477  psgnfn  18127  psgnval  18133  dchrptlem1  25209  lgsdchrval  25299  lgsdchr  25300  bnj1366  31232  nosupno  32180  nosupdm  32181  nosupbday  32182  nosupfv  32183  nosupres  32184  nosupbnd1lem1  32185  bj-finsumval0  33477  ellimciota  40358  fourierdlem36  40871
  Copyright terms: Public domain W3C validator