Metamath Proof Explorer

Theorem rnssi

Description: Subclass inference for range. (Contributed by Peter Mazsa, 24-Sep-2022)

Ref Expression
Hypothesis rnssi.1 
|- A C_ B
Assertion rnssi 
|- ran A C_ ran B

Proof

Step Hyp Ref Expression
1 rnssi.1 
 |-  A C_ B
2 rnss 
 |-  ( A C_ B -> ran A C_ ran B )
3 1 2 ax-mp 
 |-  ran A C_ ran B