Theorem cbvmptdavw

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

	Ref	Expression
Hypothesis	cbvmptdavw.1	|- ( ( ph /\ x = y ) -> B = C )
Assertion	cbvmptdavw	|- ( ph -> ( x e. A |-> B ) = ( y e. A |-> C ) )

Proof

Step	Hyp	Ref	Expression
1		cbvmptdavw.1	|- ( ( ph /\ x = y ) -> B = C )
2		eleq1w	|- ( x = y -> ( x e. A <-> y e. A ) )
3	2	adantl	|- ( ( ph /\ x = y ) -> ( x e. A <-> y e. A ) )
4	1	eqeq2d	|- ( ( ph /\ x = y ) -> ( t = B <-> t = C ) )
5	3 4	anbi12d	|- ( ( ph /\ x = y ) -> ( ( x e. A /\ t = B ) <-> ( y e. A /\ t = C ) ) )
6	5	cbvopab1davw	|- ( ph -> { <. x , t >. | ( x e. A /\ t = B ) } = { <. y , t >. | ( y e. A /\ t = C ) } )
7		df-mpt	|- ( x e. A |-> B ) = { <. x , t >. | ( x e. A /\ t = B ) }
8		df-mpt	|- ( y e. A |-> C ) = { <. y , t >. | ( y e. A /\ t = C ) }
9	6 7 8	3eqtr4g	|- ( ph -> ( x e. A |-> B ) = ( y e. A |-> C ) )