Metamath Proof Explorer


Theorem rnss

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

Ref Expression
Assertion rnss A B ran A ran B

Proof

Step Hyp Ref Expression
1 cnvss A B A -1 B -1
2 dmss A -1 B -1 dom A -1 dom B -1
3 1 2 syl A B dom A -1 dom B -1
4 df-rn ran A = dom A -1
5 df-rn ran B = dom B -1
6 3 4 5 3sstr4g A B ran A ran B