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