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

Theorem iotaex 5520
Description: Theorem 8.23 in [Quine] p. 58. This theorem proves the existence of the  iota class under our definition. (Contributed by Andrew Salmon, 11-Jul-2011.)
Assertion
Ref Expression
iotaex  |-  ( iota
x ph )  e.  _V

Proof of Theorem iotaex
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 iotaval 5514 . . . . 5  |-  ( A. x ( ph  <->  x  =  z )  ->  ( iota x ph )  =  z )
21eqcomd 2429 . . . 4  |-  ( A. x ( ph  <->  x  =  z )  ->  z  =  ( iota x ph ) )
32eximi 1701 . . 3  |-  ( E. z A. x (
ph 
<->  x  =  z )  ->  E. z  z  =  ( iota x ph ) )
4 df-eu 2275 . . 3  |-  ( E! x ph  <->  E. z A. x ( ph  <->  x  =  z ) )
5 isset 3021 . . 3  |-  ( ( iota x ph )  e.  _V  <->  E. z  z  =  ( iota x ph ) )
63, 4, 53imtr4i 269 . 2  |-  ( E! x ph  ->  ( iota x ph )  e. 
_V )
7 iotanul 5518 . . 3  |-  ( -.  E! x ph  ->  ( iota x ph )  =  (/) )
8 0ex 4494 . . 3  |-  (/)  e.  _V
97, 8syl6eqel 2509 . 2  |-  ( -.  E! x ph  ->  ( iota x ph )  e.  _V )
106, 9pm2.61i 167 1  |-  ( iota
x ph )  e.  _V
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 187   A.wal 1435    = wceq 1437   E.wex 1657    e. wcel 1872   E!weu 2271   _Vcvv 3017   (/)c0 3699   iotacio 5501
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-nul 4493
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-ral 2714  df-rex 2715  df-v 3019  df-sbc 3238  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-sn 3937  df-pr 3939  df-uni 4158  df-iota 5503
This theorem is referenced by:  iota4an  5522  fvex  5830  riotaex  6210  erov  7410  iunfictbso  8491  isf32lem9  8737  sumex  13692  prodex  13899  pcval  14732  grpidval  16441  fn0g  16443  gsumvalx  16451  psgnfn  17080  psgnval  17086  dchrptlem1  24129  lgsdchrval  24212  lgsdchr  24213  bnj1366  29588  bj-finsumval0  31609  ellimciota  37577  fourierdlem36  37889
  Copyright terms: Public domain W3C validator