Theorem mpoeq123dv

Description: An equality deduction for the maps-to notation. (Contributed by NM, 12-Sep-2011)

	Ref	Expression
Hypotheses	mpoeq123dv.1	$$⊢\phi \to A=D$$
	mpoeq123dv.2	$$⊢\phi \to B=E$$
	mpoeq123dv.3	$$⊢\phi \to C=F$$
Assertion	mpoeq123dv	$$⊢\phi \to \left(x\in A,y\in B⟼C\right)=\left(x\in D,y\in E⟼F\right)$$

Proof

Step	Hyp	Ref	Expression
1		mpoeq123dv.1	$$⊢\phi \to A=D$$
2		mpoeq123dv.2	$$⊢\phi \to B=E$$
3		mpoeq123dv.3	$$⊢\phi \to C=F$$
4	2	adantr	$$⊢\left(\phi \wedge x\in A\right)\to B=E$$
5	3	adantr	$$⊢\left(\phi \wedge \left(x\in A\wedge y\in B\right)\right)\to C=F$$
6	1 4 5	mpoeq123dva	$$⊢\phi \to \left(x\in A,y\in B⟼C\right)=\left(x\in D,y\in E⟼F\right)$$