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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | resres | |
|
2 | ssid | |
|
3 | resmpt | |
|
4 | 2 3 | ax-mp | |
5 | 4 | reseq1i | |
6 | inss1 | |
|
7 | resmpt | |
|
8 | 6 7 | ax-mp | |
9 | 1 5 8 | 3eqtr3i | |