Metamath Proof Explorer

Theorem resimass

Description: The image of a restriction is a subset of the original image. (Contributed by Glauco Siliprandi, 23-Oct-2021)

		Ref	Expression
	Assertion	resimass	$⊢ ({A ↾}_{B}) [C] \subseteq A [C]$

Step	Hyp	Ref	Expression
1		resss	$⊢ {A ↾}_{B} \subseteq A$
2		imass1	$⊢ {A ↾}_{B} \subseteq A \to ({A ↾}_{B}) [C] \subseteq A [C]$
3	1 2	ax-mp	$⊢ ({A ↾}_{B}) [C] \subseteq A [C]$