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 abbi1
 |-  ( 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 ) )