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

Metamath Proof Explorer

Theorem resabs2d

Description: Absorption law for restriction. (Contributed by Glauco Siliprandi, 23-Oct-2021)

		Ref	Expression
	Hypothesis	resabs2d.1	$⊢ φ \to B \subseteq C$
	Assertion	resabs2d	$⊢ φ \to {({A ↾}_{B}) ↾}_{C} = {A ↾}_{B}$

Step	Hyp	Ref	Expression
1		resabs2d.1	$⊢ φ \to B \subseteq C$
2		resabs2	$⊢ B \subseteq C \to {({A ↾}_{B}) ↾}_{C} = {A ↾}_{B}$
3	1 2	syl	$⊢ φ \to {({A ↾}_{B}) ↾}_{C} = {A ↾}_{B}$