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

Metamath Proof Explorer

Theorem resabs2

Description: Absorption law for restriction. (Contributed by NM, 27-Mar-1998)

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

Proof

Step Hyp Ref Expression
1 rescom ⊢ A ↾ B ↾ C = A ↾ C ↾ B
2 resabs1 ⊢ B ⊆ C → A ↾ C ↾ B = A ↾ B
3 1 2 eqtrid ⊢ B ⊆ C → A ↾ B ↾ C = A ↾ B