Metamath Proof Explorer


Theorem rnssi

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

Ref Expression
Hypothesis rnssi.1 A B
Assertion rnssi ran A ran B

Proof

Step Hyp Ref Expression
1 rnssi.1 A B
2 rnss A B ran A ran B
3 1 2 ax-mp ran A ran B