imass2

Description: Subset theorem for image. Exercise 22(a) of Enderton p. 53. (Contributed by NM, 22-Mar-1998)

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

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

Metamath Proof Explorer