Theorem mpteq12df

Description: An equality inference for the maps-to notation. Compare mpteq12dv . (Contributed by Scott Fenton, 8-Aug-2013) (Revised by Mario Carneiro, 11-Dec-2016)

	Ref	Expression
Hypotheses	mpteq12df.1	$$⊢Ⅎx\phi$$
	mpteq12df.2	$$⊢\phi \to A=C$$
	mpteq12df.3	$$⊢\phi \to B=D$$
Assertion	mpteq12df	$$⊢\phi \to \left(x\in A⟼B\right)=\left(x\in C⟼D\right)$$

Proof

Step	Hyp	Ref	Expression
1		mpteq12df.1	$$⊢Ⅎx\phi$$
2		mpteq12df.2	$$⊢\phi \to A=C$$
3		mpteq12df.3	$$⊢\phi \to B=D$$
4		nfv	$$⊢Ⅎy\phi$$
5	2	eleq2d	$$⊢\phi \to \left(x\in A\leftrightarrow x\in C\right)$$
6	3	eqeq2d	$$⊢\phi \to \left(y=B\leftrightarrow y=D\right)$$
7	5 6	anbi12d	$$⊢\phi \to \left(\left(x\in A\wedge y=B\right)\leftrightarrow \left(x\in C\wedge y=D\right)\right)$$
8	1 4 7	opabbid	$$⊢\phi \to \left\{⟨x,y⟩|\left(x\in A\wedge y=B\right)\right\}=\left\{⟨x,y⟩|\left(x\in C\wedge y=D\right)\right\}$$
9		df-mpt	$$⊢\left(x\in A⟼B\right)=\left\{⟨x,y⟩|\left(x\in A\wedge y=B\right)\right\}$$
10		df-mpt	$$⊢\left(x\in C⟼D\right)=\left\{⟨x,y⟩|\left(x\in C\wedge y=D\right)\right\}$$
11	8 9 10	3eqtr4g	$$⊢\phi \to \left(x\in A⟼B\right)=\left(x\in C⟼D\right)$$