Metamath Proof Explorer


Theorem resmpt

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

Ref Expression
Assertion resmpt BAxACB=xBC

Proof

Step Hyp Ref Expression
1 resopab2 BAxy|xAy=CB=xy|xBy=C
2 df-mpt xAC=xy|xAy=C
3 2 reseq1i xACB=xy|xAy=CB
4 df-mpt xBC=xy|xBy=C
5 1 3 4 3eqtr4g BAxACB=xBC