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

Metamath Proof Explorer

Theorem iota1

Description: Property of iota. (Contributed by NM, 23-Aug-2011) (Revised by Mario Carneiro, 23-Dec-2016)

Ref Expression
Assertion iota1 
|- ( E! x ph -> ( ph <-> ( iota x ph ) = x ) )

Proof

Step Hyp Ref Expression
1 eu6 
 |-  ( E! x ph <-> E. z A. x ( ph <-> x = z ) )
2 sp 
 |-  ( A. x ( ph <-> x = z ) -> ( ph <-> x = z ) )
3 iotaval 
 |-  ( A. x ( ph <-> x = z ) -> ( iota x ph ) = z )
4 3 eqeq2d 
 |-  ( A. x ( ph <-> x = z ) -> ( x = ( iota x ph ) <-> x = z ) )
5 2 4 bitr4d 
 |-  ( A. x ( ph <-> x = z ) -> ( ph <-> x = ( iota x ph ) ) )
6 eqcom 
 |-  ( x = ( iota x ph ) <-> ( iota x ph ) = x )
7 5 6 bitrdi 
 |-  ( A. x ( ph <-> x = z ) -> ( ph <-> ( iota x ph ) = x ) )
8 7 exlimiv 
 |-  ( E. z A. x ( ph <-> x = z ) -> ( ph <-> ( iota x ph ) = x ) )
9 1 8 sylbi 
 |-  ( E! x ph -> ( ph <-> ( iota x ph ) = x ) )