Theorem iotabi

Description: Equivalence theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011)

	Ref	Expression
Assertion	iotabi	|- ( A. x ( ph <-> ps ) -> ( iota x ph ) = ( iota x ps ) )

Proof

Step	Hyp	Ref	Expression
1		abbi1	|- ( A. x ( ph <-> ps ) -> { x | ph } = { x | ps } )
2	1	eqeq1d	|- ( A. x ( ph <-> ps ) -> ( { x | ph } = { z } <-> { x | ps } = { z } ) )
3	2	abbidv	|- ( A. x ( ph <-> ps ) -> { z | { x | ph } = { z } } = { z | { x | ps } = { z } } )
4	3	unieqd	|- ( A. x ( ph <-> ps ) -> U. { z | { x | ph } = { z } } = U. { z | { x | ps } = { z } } )
5		df-iota	|- ( iota x ph ) = U. { z | { x | ph } = { z } }
6		df-iota	|- ( iota x ps ) = U. { z | { x | ps } = { z } }
7	4 5 6	3eqtr4g	|- ( A. x ( ph <-> ps ) -> ( iota x ph ) = ( iota x ps ) )