Theorem rnss

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

	Ref	Expression
Assertion	rnss	|- ( A C_ B -> ran A C_ ran B )

Proof

Step	Hyp	Ref	Expression
1		cnvss	|- ( A C_ B -> `' A C_ `' B )
2		dmss	|- ( `' A C_ `' B -> dom `' A C_ dom `' B )
3	1 2	syl	|- ( A C_ B -> dom `' A C_ dom `' B )
4		df-rn	|- ran A = dom `' A
5		df-rn	|- ran B = dom `' B
6	3 4 5	3sstr4g	|- ( A C_ B -> ran A C_ ran B )