Metamath Proof Explorer


Theorem resmpo

Description: Restriction of the mapping operation. (Contributed by Mario Carneiro, 17-Dec-2013)

Ref Expression
Assertion resmpo CADBxA,yBEC×D=xC,yDE

Proof

Step Hyp Ref Expression
1 resoprab2 CADBxyz|xAyBz=EC×D=xyz|xCyDz=E
2 df-mpo xA,yBE=xyz|xAyBz=E
3 2 reseq1i xA,yBEC×D=xyz|xAyBz=EC×D
4 df-mpo xC,yDE=xyz|xCyDz=E
5 1 3 4 3eqtr4g CADBxA,yBEC×D=xC,yDE