This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iotain

Description: Equivalence between two different forms of iota . (Contributed by Andrew Salmon, 15-Jul-2011)

Ref Expression
Assertion iotain 
|- ( E! x ph -> |^| { x | ph } = ( iota x ph ) )

Proof

Step Hyp Ref Expression
1 eu6 
 |-  ( E! x ph <-> E. y A. x ( ph <-> x = y ) )
2 vex 
 |-  y e. _V
3 2 intsn 
 |-  |^| { y } = y
4 abbi 
 |-  ( A. x ( ph <-> x = y ) -> { x | ph } = { x | x = y } )
5 df-sn 
 |-  { y } = { x | x = y }
6 4 5 eqtr4di 
 |-  ( A. x ( ph <-> x = y ) -> { x | ph } = { y } )
7 6 inteqd 
 |-  ( A. x ( ph <-> x = y ) -> |^| { x | ph } = |^| { y } )
8 iotaval 
 |-  ( A. x ( ph <-> x = y ) -> ( iota x ph ) = y )
9 3 7 8 3eqtr4a 
 |-  ( A. x ( ph <-> x = y ) -> |^| { x | ph } = ( iota x ph ) )
10 9 exlimiv 
 |-  ( E. y A. x ( ph <-> x = y ) -> |^| { x | ph } = ( iota x ph ) )
11 1 10 sylbi 
 |-  ( E! x ph -> |^| { x | ph } = ( iota x ph ) )