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

Theorem iotaex 5856
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 5850 . . . . 5 (∀𝑥(𝜑𝑥 = 𝑧) → (℩𝑥𝜑) = 𝑧)
21eqcomd 2626 . . . 4 (∀𝑥(𝜑𝑥 = 𝑧) → 𝑧 = (℩𝑥𝜑))
32eximi 1760 . . 3 (∃𝑧𝑥(𝜑𝑥 = 𝑧) → ∃𝑧 𝑧 = (℩𝑥𝜑))
4 df-eu 2472 . . 3 (∃!𝑥𝜑 ↔ ∃𝑧𝑥(𝜑𝑥 = 𝑧))
5 isset 3202 . . 3 ((℩𝑥𝜑) ∈ V ↔ ∃𝑧 𝑧 = (℩𝑥𝜑))
63, 4, 53imtr4i 281 . 2 (∃!𝑥𝜑 → (℩𝑥𝜑) ∈ V)
7 iotanul 5854 . . 3 (¬ ∃!𝑥𝜑 → (℩𝑥𝜑) = ∅)
8 0ex 4781 . . 3 ∅ ∈ V
97, 8syl6eqel 2707 . 2 (¬ ∃!𝑥𝜑 → (℩𝑥𝜑) ∈ V)
106, 9pm2.61i 176 1 (℩𝑥𝜑) ∈ V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wal 1479   = wceq 1481  wex 1702  wcel 1988  ∃!weu 2468  Vcvv 3195  c0 3907  cio 5837
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-nul 4780
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-sn 4169  df-pr 4171  df-uni 4428  df-iota 5839
This theorem is referenced by:  iota4an  5858  fvex  6188  riotaex  6600  erov  7829  iunfictbso  8922  isf32lem9  9168  sumex  14399  prodex  14618  pcval  15530  grpidval  17241  fn0g  17243  gsumvalx  17251  psgnfn  17902  psgnval  17908  dchrptlem1  24970  lgsdchrval  25060  lgsdchr  25061  bnj1366  30874  nosupno  31823  nosupdm  31824  nosupbday  31825  nosupfv  31826  nosupres  31827  nosupbnd1lem1  31828  bj-finsumval0  33118  ellimciota  39646  fourierdlem36  40123
  Copyright terms: Public domain W3C validator