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

Theorem iotaex 5438
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 5432 . . . . 5  |-  ( A. x ( ph  <->  x  =  z )  ->  ( iota x ph )  =  z )
21eqcomd 2443 . . . 4  |-  ( A. x ( ph  <->  x  =  z )  ->  z  =  ( iota x ph ) )
32eximi 1586 . . 3  |-  ( E. z A. x (
ph 
<->  x  =  z )  ->  E. z  z  =  ( iota x ph ) )
4 df-eu 2287 . . 3  |-  ( E! x ph  <->  E. z A. x ( ph  <->  x  =  z ) )
5 isset 2962 . . 3  |-  ( ( iota x ph )  e.  _V  <->  E. z  z  =  ( iota x ph ) )
63, 4, 53imtr4i 259 . 2  |-  ( E! x ph  ->  ( iota x ph )  e. 
_V )
7 iotanul 5436 . . 3  |-  ( -.  E! x ph  ->  ( iota x ph )  =  (/) )
8 0ex 4342 . . 3  |-  (/)  e.  _V
97, 8syl6eqel 2526 . 2  |-  ( -.  E! x ph  ->  ( iota x ph )  e.  _V )
106, 9pm2.61i 159 1  |-  ( iota
x ph )  e.  _V
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 178   A.wal 1550   E.wex 1551    = wceq 1653    e. wcel 1726   E!weu 2283   _Vcvv 2958   (/)c0 3630   iotacio 5419
This theorem is referenced by:  iota4an  5440  fvex  5745  riotaex  6556  erov  7004  iunfictbso  8000  isf32lem9  8246  sumex  12486  pcval  13223  grpidval  14712  fn0g  14713  gsumvalx  14779  dchrptlem1  21053  lgsdchrval  21136  lgsdchr  21137  prodex  25238  psgnfn  27415  psgnval  27421  bnj1366  29275
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-nul 4341
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-v 2960  df-sbc 3164  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-sn 3822  df-pr 3823  df-uni 4018  df-iota 5421
  Copyright terms: Public domain W3C validator