Theorem cbviotadavw

Description: Change bound variable in a description binder. Deduction form. (Contributed by GG, 14-Aug-2025)

	Ref	Expression
Hypothesis	cbviotadavw.1	|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )
Assertion	cbviotadavw	|- ( ph -> ( iota x ps ) = ( iota y ch ) )

Proof

Step	Hyp	Ref	Expression
1		cbviotadavw.1	|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )
2	1	cbvabdavw	|- ( ph -> { x | ps } = { y | ch } )
3	2	eqeq1d	|- ( ph -> ( { x | ps } = { t } <-> { y | ch } = { t } ) )
4	3	abbidv	|- ( ph -> { t | { x | ps } = { t } } = { t | { y | ch } = { t } } )
5	4	unieqd	|- ( ph -> U. { t | { x | ps } = { t } } = U. { t | { y | ch } = { t } } )
6		df-iota	|- ( iota x ps ) = U. { t | { x | ps } = { t } }
7		df-iota	|- ( iota y ch ) = U. { t | { y | ch } = { t } }
8	5 6 7	3eqtr4g	|- ( ph -> ( iota x ps ) = ( iota y ch ) )