Theorem rnss

Description: Subset theorem for range. (Contributed by NM, 22-Mar-1998)

	Ref	Expression
Assertion	rnss	$$⊢A\subseteq B\to \mathrm{ran}A\subseteq \mathrm{ran}B$$

Proof

Step	Hyp	Ref	Expression
1		cnvss	$$⊢A\subseteq B\to A^{-1}\subseteq B^{-1}$$
2		dmss	$$⊢A^{-1}\subseteq B^{-1}\to \mathrm{dom}{A}^{-1}\subseteq \mathrm{dom}{B}^{-1}$$
3	1 2	syl	$$⊢A\subseteq B\to \mathrm{dom}{A}^{-1}\subseteq \mathrm{dom}{B}^{-1}$$
4		df-rn	$$⊢\mathrm{ran}A=\mathrm{dom}{A}^{-1}$$
5		df-rn	$$⊢\mathrm{ran}B=\mathrm{dom}{B}^{-1}$$
6	3 4 5	3sstr4g	$$⊢A\subseteq B\to \mathrm{ran}A\subseteq \mathrm{ran}B$$