Theorem cbvmptdavw2

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

	Ref	Expression
Hypotheses	cbvmptdavw2.1	|- ( ( ph /\ x = y ) -> C = D )
	cbvmptdavw2.2	|- ( ( ph /\ x = y ) -> A = B )
Assertion	cbvmptdavw2	|- ( ph -> ( x e. A |-> C ) = ( y e. B |-> D ) )

Proof

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