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

Metamath Proof Explorer

Theorem resabs1

Description: Absorption law for restriction. Exercise 17 of TakeutiZaring p. 25. (Contributed by NM, 9-Aug-1994)

Ref Expression
Assertion resabs1 ⊢ B ⊆ C → A ↾ C ↾ B = A ↾ B

Proof

Step Hyp Ref Expression
1 resres ⊢ A ↾ C ↾ B = A ↾ C ∩ B
2 sseqin2 ⊢ B ⊆ C ↔ C ∩ B = B
3 reseq2 ⊢ C ∩ B = B → A ↾ C ∩ B = A ↾ B
4 2 3 sylbi ⊢ B ⊆ C → A ↾ C ∩ B = A ↾ B
5 1 4 eqtrid ⊢ B ⊆ C → A ↾ C ↾ B = A ↾ B