Theorem cbvmpo1vw2

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

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

Proof

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