Metamath Proof Explorer


Theorem subrngss

Description: A subring is a subset. (Contributed by AV, 14-Feb-2025)

Ref Expression
Hypothesis subrngss.1 B = Base R
Assertion subrngss A SubRng R A B

Proof

Step Hyp Ref Expression
1 subrngss.1 B = Base R
2 1 issubrng A SubRng R R Rng R 𝑠 A Rng A B
3 2 simp3bi A SubRng R A B