Theorem cbvmpovw2

Description: Change bound variables and domains in a maps-to function, using implicit substitution. (Contributed by GG, 14-Aug-2025)

	Ref	Expression
Hypotheses	cbvmpovw2.1	|- ( ( x = z /\ y = w ) -> E = F )
	cbvmpovw2.2	|- ( ( x = z /\ y = w ) -> C = D )
	cbvmpovw2.3	|- ( ( x = z /\ y = w ) -> A = B )
Assertion	cbvmpovw2	|- ( x e. A , y e. C |-> E ) = ( z e. B , w e. D |-> F )

Proof

Step	Hyp	Ref	Expression
1		cbvmpovw2.1	|- ( ( x = z /\ y = w ) -> E = F )
2		cbvmpovw2.2	|- ( ( x = z /\ y = w ) -> C = D )
3		cbvmpovw2.3	|- ( ( x = z /\ y = w ) -> A = B )
4		simpl	|- ( ( x = z /\ y = w ) -> x = z )
5	4 3	eleq12d	|- ( ( x = z /\ y = w ) -> ( x e. A <-> z e. B ) )
6		simpr	|- ( ( x = z /\ y = w ) -> y = w )
7	6 2	eleq12d	|- ( ( x = z /\ y = w ) -> ( y e. C <-> w e. D ) )
8	5 7	anbi12d	|- ( ( x = z /\ y = w ) -> ( ( x e. A /\ y e. C ) <-> ( z e. B /\ w e. D ) ) )
9	1	eqeq2d	|- ( ( x = z /\ y = w ) -> ( t = E <-> t = F ) )
10	8 9	anbi12d	|- ( ( x = z /\ y = w ) -> ( ( ( x e. A /\ y e. C ) /\ t = E ) <-> ( ( z e. B /\ w e. D ) /\ t = F ) ) )
11	10	cbvoprab12v	|- { <. <. x , y >. , t >. | ( ( x e. A /\ y e. C ) /\ t = E ) } = { <. <. z , w >. , t >. | ( ( z e. B /\ w e. D ) /\ t = F ) }
12		df-mpo	|- ( x e. A , y e. C |-> E ) = { <. <. x , y >. , t >. | ( ( x e. A /\ y e. C ) /\ t = E ) }
13		df-mpo	|- ( z e. B , w e. D |-> F ) = { <. <. z , w >. , t >. | ( ( z e. B /\ w e. D ) /\ t = F ) }
14	11 12 13	3eqtr4i	|- ( x e. A , y e. C |-> E ) = ( z e. B , w e. D |-> F )