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	$$⊢\left(x=z\wedge y=w\right)\to E=F$$
	cbvmpovw2.2	$$⊢\left(x=z\wedge y=w\right)\to C=D$$
	cbvmpovw2.3	$$⊢\left(x=z\wedge y=w\right)\to A=B$$
Assertion	cbvmpovw2	$$⊢\left(x\in A,y\in C⟼E\right)=\left(z\in B,w\in D⟼F\right)$$

Proof

Step	Hyp	Ref	Expression
1		cbvmpovw2.1	$$⊢\left(x=z\wedge y=w\right)\to E=F$$
2		cbvmpovw2.2	$$⊢\left(x=z\wedge y=w\right)\to C=D$$
3		cbvmpovw2.3	$$⊢\left(x=z\wedge y=w\right)\to A=B$$
4		simpl	$$⊢\left(x=z\wedge y=w\right)\to x=z$$
5	4 3	eleq12d	$$⊢\left(x=z\wedge y=w\right)\to \left(x\in A\leftrightarrow z\in B\right)$$
6		simpr	$$⊢\left(x=z\wedge y=w\right)\to y=w$$
7	6 2	eleq12d	$$⊢\left(x=z\wedge y=w\right)\to \left(y\in C\leftrightarrow w\in D\right)$$
8	5 7	anbi12d	$$⊢\left(x=z\wedge y=w\right)\to \left(\left(x\in A\wedge y\in C\right)\leftrightarrow \left(z\in B\wedge w\in D\right)\right)$$
9	1	eqeq2d	$$⊢\left(x=z\wedge y=w\right)\to \left(t=E\leftrightarrow t=F\right)$$
10	8 9	anbi12d	$$⊢\left(x=z\wedge y=w\right)\to \left(\left(\left(x\in A\wedge y\in C\right)\wedge t=E\right)\leftrightarrow \left(\left(z\in B\wedge w\in D\right)\wedge t=F\right)\right)$$
11	10	cbvoprab12v	$$⊢\left\{⟨⟨x,y⟩,t⟩|\left(\left(x\in A\wedge y\in C\right)\wedge t=E\right)\right\}=\left\{⟨⟨z,w⟩,t⟩|\left(\left(z\in B\wedge w\in D\right)\wedge t=F\right)\right\}$$
12		df-mpo	$$⊢\left(x\in A,y\in C⟼E\right)=\left\{⟨⟨x,y⟩,t⟩|\left(\left(x\in A\wedge y\in C\right)\wedge t=E\right)\right\}$$
13		df-mpo	$$⊢\left(z\in B,w\in D⟼F\right)=\left\{⟨⟨z,w⟩,t⟩|\left(\left(z\in B\wedge w\in D\right)\wedge t=F\right)\right\}$$
14	11 12 13	3eqtr4i	$$⊢\left(x\in A,y\in C⟼E\right)=\left(z\in B,w\in D⟼F\right)$$