Metamath Proof Explorer

Theorem rnresss

Description: The range of a restriction is a subset of the whole range. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion rnresss 
|- ran ( A |` B ) C_ ran A

Proof

Step Hyp Ref Expression
1 resss 
 |-  ( A |` B ) C_ A
2 1 rnssi 
 |-  ran ( A |` B ) C_ ran A