Theorem iotaint

Description: Equivalence between two different forms of iota . (Contributed by Mario Carneiro, 24-Dec-2016)

	Ref	Expression
Assertion	iotaint	|- ( E! x ph -> ( iota x ph ) = |^| { x | ph } )

Proof

Step	Hyp	Ref	Expression
1		iotauni	|- ( E! x ph -> ( iota x ph ) = U. { x | ph } )
2		uniintab	|- ( E! x ph <-> U. { x | ph } = |^| { x | ph } )
3	2	biimpi	|- ( E! x ph -> U. { x | ph } = |^| { x | ph } )
4	1 3	eqtrd	|- ( E! x ph -> ( iota x ph ) = |^| { x | ph } )