Description: Subclass inference for range. (Contributed by Peter Mazsa, 24Sep2022)
Ref  Expression  

Hypothesis  rnssi.1   A C_ B 

Assertion  rnssi   ran A C_ ran B 
Step  Hyp  Ref  Expression 

1  rnssi.1   A C_ B 

2  rnss   ( A C_ B > ran A C_ ran B ) 

3  1 2  axmp   ran A C_ ran B 