Theorem imass1

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

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

Proof

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