Theorem cbvmpo2vw2

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

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

Proof

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