Theorem mpoeq12

Description: An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013)

	Ref	Expression
Assertion	mpoeq12	$$⊢\left(A=C\wedge B=D\right)\to \left(x\in A,y\in B⟼E\right)=\left(x\in C,y\in D⟼E\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢E=E$$
2	1	rgenw	$$⊢\forall y\in BE=E$$
3	2	jctr	$$⊢B=D\to \left(B=D\wedge \forall y\in BE=E\right)$$
4	3	ralrimivw	$$⊢B=D\to \forall x\in A\left(B=D\wedge \forall y\in BE=E\right)$$
5		mpoeq123	$$⊢\left(A=C\wedge \forall x\in A\left(B=D\wedge \forall y\in BE=E\right)\right)\to \left(x\in A,y\in B⟼E\right)=\left(x\in C,y\in D⟼E\right)$$
6	4 5	sylan2	$$⊢\left(A=C\wedge B=D\right)\to \left(x\in A,y\in B⟼E\right)=\left(x\in C,y\in D⟼E\right)$$