# Metamath Proof Explorer

## Theorem ressabs

Description: Restriction absorption law. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Assertion ressabs ${⊢}\left({A}\in {X}\wedge {B}\subseteq {A}\right)\to \left({W}{↾}_{𝑠}{A}\right){↾}_{𝑠}{B}={W}{↾}_{𝑠}{B}$

### Proof

Step Hyp Ref Expression
1 ssexg ${⊢}\left({B}\subseteq {A}\wedge {A}\in {X}\right)\to {B}\in \mathrm{V}$
2 1 ancoms ${⊢}\left({A}\in {X}\wedge {B}\subseteq {A}\right)\to {B}\in \mathrm{V}$
3 ressress ${⊢}\left({A}\in {X}\wedge {B}\in \mathrm{V}\right)\to \left({W}{↾}_{𝑠}{A}\right){↾}_{𝑠}{B}={W}{↾}_{𝑠}\left({A}\cap {B}\right)$
4 2 3 syldan ${⊢}\left({A}\in {X}\wedge {B}\subseteq {A}\right)\to \left({W}{↾}_{𝑠}{A}\right){↾}_{𝑠}{B}={W}{↾}_{𝑠}\left({A}\cap {B}\right)$
5 simpr ${⊢}\left({A}\in {X}\wedge {B}\subseteq {A}\right)\to {B}\subseteq {A}$
6 sseqin2 ${⊢}{B}\subseteq {A}↔{A}\cap {B}={B}$
7 5 6 sylib ${⊢}\left({A}\in {X}\wedge {B}\subseteq {A}\right)\to {A}\cap {B}={B}$
8 7 oveq2d ${⊢}\left({A}\in {X}\wedge {B}\subseteq {A}\right)\to {W}{↾}_{𝑠}\left({A}\cap {B}\right)={W}{↾}_{𝑠}{B}$
9 4 8 eqtrd ${⊢}\left({A}\in {X}\wedge {B}\subseteq {A}\right)\to \left({W}{↾}_{𝑠}{A}\right){↾}_{𝑠}{B}={W}{↾}_{𝑠}{B}$