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

Proof

Step	Hyp	Ref	Expression
1		cbvmpo1vw2.1	$$⊢x=z\to E=F$$
2		cbvmpo1vw2.2	$$⊢x=z\to C=D$$
3		cbvmpo1vw2.3	$$⊢x=z\to A=B$$
4		id	$$⊢x=z\to x=z$$
5	4 3	eleq12d	$$⊢x=z\to \left(x\in A\leftrightarrow z\in B\right)$$
6	2	eleq2d	$$⊢x=z\to \left(y\in C\leftrightarrow y\in D\right)$$
7	5 6	anbi12d	$$⊢x=z\to \left(\left(x\in A\wedge y\in C\right)\leftrightarrow \left(z\in B\wedge y\in D\right)\right)$$
8	1	eqeq2d	$$⊢x=z\to \left(t=E\leftrightarrow t=F\right)$$
9	7 8	anbi12d	$$⊢x=z\to \left(\left(\left(x\in A\wedge y\in C\right)\wedge t=E\right)\leftrightarrow \left(\left(z\in B\wedge y\in D\right)\wedge t=F\right)\right)$$
10	9	cbvoprab1vw	$$⊢\left\{⟨⟨x,y⟩,t⟩|\left(\left(x\in A\wedge y\in C\right)\wedge t=E\right)\right\}=\left\{⟨⟨z,y⟩,t⟩|\left(\left(z\in B\wedge y\in D\right)\wedge t=F\right)\right\}$$
11		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\}$$
12		df-mpo	$$⊢\left(z\in B,y\in D⟼F\right)=\left\{⟨⟨z,y⟩,t⟩|\left(\left(z\in B\wedge y\in D\right)\wedge t=F\right)\right\}$$
13	10 11 12	3eqtr4i	$$⊢\left(x\in A,y\in C⟼E\right)=\left(z\in B,y\in D⟼F\right)$$