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

Theorem iotaex 5551
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 5545 . . . . 5  |-  ( A. x ( ph  <->  x  =  z )  ->  ( iota x ph )  =  z )
21eqcomd 2462 . . . 4  |-  ( A. x ( ph  <->  x  =  z )  ->  z  =  ( iota x ph ) )
32eximi 1661 . . 3  |-  ( E. z A. x (
ph 
<->  x  =  z )  ->  E. z  z  =  ( iota x ph ) )
4 df-eu 2288 . . 3  |-  ( E! x ph  <->  E. z A. x ( ph  <->  x  =  z ) )
5 isset 3110 . . 3  |-  ( ( iota x ph )  e.  _V  <->  E. z  z  =  ( iota x ph ) )
63, 4, 53imtr4i 266 . 2  |-  ( E! x ph  ->  ( iota x ph )  e. 
_V )
7 iotanul 5549 . . 3  |-  ( -.  E! x ph  ->  ( iota x ph )  =  (/) )
8 0ex 4569 . . 3  |-  (/)  e.  _V
97, 8syl6eqel 2550 . 2  |-  ( -.  E! x ph  ->  ( iota x ph )  e.  _V )
106, 9pm2.61i 164 1  |-  ( iota
x ph )  e.  _V
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184   A.wal 1396    = wceq 1398   E.wex 1617    e. wcel 1823   E!weu 2284   _Vcvv 3106   (/)c0 3783   iotacio 5532
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-nul 4568
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-sn 4017  df-pr 4019  df-uni 4236  df-iota 5534
This theorem is referenced by:  iota4an  5553  fvex  5858  riotaex  6236  erov  7400  iunfictbso  8486  isf32lem9  8732  sumex  13592  prodex  13796  pcval  14452  grpidval  16086  fn0g  16088  gsumvalx  16096  psgnfn  16725  psgnval  16731  dchrptlem1  23737  lgsdchrval  23820  lgsdchr  23821  ellimciota  31859  fourierdlem36  32164  bnj1366  34289  bj-finsumval0  35063
  Copyright terms: Public domain W3C validator