Theorem cbvmptvw2

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

	Ref	Expression
Hypotheses	cbvmptvw2.1	$$⊢x=y\to C=D$$
	cbvmptvw2.2	$$⊢x=y\to A=B$$
Assertion	cbvmptvw2	$$⊢\left(x\in A⟼C\right)=\left(y\in B⟼D\right)$$

Proof

Step	Hyp	Ref	Expression
1		cbvmptvw2.1	$$⊢x=y\to C=D$$
2		cbvmptvw2.2	$$⊢x=y\to A=B$$
3		eleq1w	$$⊢x=y\to \left(x\in A\leftrightarrow y\in A\right)$$
4	2	eleq2d	$$⊢x=y\to \left(y\in A\leftrightarrow y\in B\right)$$
5	3 4	bitrd	$$⊢x=y\to \left(x\in A\leftrightarrow y\in B\right)$$
6	1	eqeq2d	$$⊢x=y\to \left(t=C\leftrightarrow t=D\right)$$
7	5 6	anbi12d	$$⊢x=y\to \left(\left(x\in A\wedge t=C\right)\leftrightarrow \left(y\in B\wedge t=D\right)\right)$$
8	7	cbvopab1v	$$⊢\left\{⟨x,t⟩|\left(x\in A\wedge t=C\right)\right\}=\left\{⟨y,t⟩|\left(y\in B\wedge t=D\right)\right\}$$
9		df-mpt	$$⊢\left(x\in A⟼C\right)=\left\{⟨x,t⟩|\left(x\in A\wedge t=C\right)\right\}$$
10		df-mpt	$$⊢\left(y\in B⟼D\right)=\left\{⟨y,t⟩|\left(y\in B\wedge t=D\right)\right\}$$
11	8 9 10	3eqtr4i	$$⊢\left(x\in A⟼C\right)=\left(y\in B⟼D\right)$$