This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem resmpo

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

Ref Expression
Assertion resmpo 
|- ( ( C C_ A /\ D C_ B ) -> ( ( x e. A , y e. B |-> E ) |` ( C X. D ) ) = ( x e. C , y e. D |-> E ) )

Proof

Step Hyp Ref Expression
1 resoprab2 
 |-  ( ( C C_ A /\ D C_ B ) -> ( { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = E ) } |` ( C X. D ) ) = { <. <. x , y >. , z >. | ( ( x e. C /\ y e. D ) /\ z = E ) } )
2 df-mpo 
 |-  ( x e. A , y e. B |-> E ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = E ) }
3 2 reseq1i 
 |-  ( ( x e. A , y e. B |-> E ) |` ( C X. D ) ) = ( { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = E ) } |` ( C X. D ) )
4 df-mpo 
 |-  ( x e. C , y e. D |-> E ) = { <. <. x , y >. , z >. | ( ( x e. C /\ y e. D ) /\ z = E ) }
5 1 3 4 3eqtr4g 
 |-  ( ( C C_ A /\ D C_ B ) -> ( ( x e. A , y e. B |-> E ) |` ( C X. D ) ) = ( x e. C , y e. D |-> E ) )