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