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

Metamath Proof Explorer

Theorem imass1

Description: Subset theorem for image. (Contributed by NM, 16-Mar-2004)

		Ref	Expression
	Assertion	imass1	$⊢ A \subseteq B \to A [C] \subseteq B [C]$

Step	Hyp	Ref	Expression
1		ssres	$⊢ A \subseteq B \to {A ↾}_{C} \subseteq {B ↾}_{C}$
2		rnss	$⊢ {A ↾}_{C} \subseteq {B ↾}_{C} \to ran ({A ↾}_{C}) \subseteq ran ({B ↾}_{C})$
3	1 2	syl	$⊢ A \subseteq B \to ran ({A ↾}_{C}) \subseteq ran ({B ↾}_{C})$
4		df-ima	$⊢ A [C] = ran ({A ↾}_{C})$
5		df-ima	$⊢ B [C] = ran ({B ↾}_{C})$
6	3 4 5	3sstr4g	$⊢ A \subseteq B \to A [C] \subseteq B [C]$