Metamath Proof Explorer


Theorem resmpt3

Description: Unconditional restriction of the mapping operation. (Contributed by Stefan O'Rear, 24-Jan-2015) (Proof shortened by Mario Carneiro, 22-Mar-2015)

Ref Expression
Assertion resmpt3 xACB=xABC

Proof

Step Hyp Ref Expression
1 resres xACAB=xACAB
2 ssid AA
3 resmpt AAxACA=xAC
4 2 3 ax-mp xACA=xAC
5 4 reseq1i xACAB=xACB
6 inss1 ABA
7 resmpt ABAxACAB=xABC
8 6 7 ax-mp xACAB=xABC
9 1 5 8 3eqtr3i xACB=xABC