Metamath Proof Explorer


Theorem subrngbas

Description: Base set of a subring structure. (Contributed by AV, 14-Feb-2025)

Ref Expression
Hypothesis subrng0.1 S = R 𝑠 A
Assertion subrngbas A SubRng R A = Base S

Proof

Step Hyp Ref Expression
1 subrng0.1 S = R 𝑠 A
2 subrngsubg A SubRng R A SubGrp R
3 1 subgbas A SubGrp R A = Base S
4 2 3 syl A SubRng R A = Base S