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