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

Proof

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