Theorem iotauni

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

	Ref	Expression
Assertion	iotauni	|- ( E! x ph -> ( iota x ph ) = U. { x | ph } )

Proof

Step	Hyp	Ref	Expression
1		eu6	|- ( E! x ph <-> E. z A. x ( ph <-> x = z ) )
2		iotaval	|- ( A. x ( ph <-> x = z ) -> ( iota x ph ) = z )
3		uniabio	|- ( A. x ( ph <-> x = z ) -> U. { x | ph } = z )
4	2 3	eqtr4d	|- ( A. x ( ph <-> x = z ) -> ( iota x ph ) = U. { x | ph } )
5	4	exlimiv	|- ( E. z A. x ( ph <-> x = z ) -> ( iota x ph ) = U. { x | ph } )
6	1 5	sylbi	|- ( E! x ph -> ( iota x ph ) = U. { x | ph } )