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 |`s A )
Assertion subrngbas 
|- ( A e. ( SubRng ` R ) -> A = ( Base ` S ) )

Proof

Step Hyp Ref Expression
1 subrng0.1 
 |-  S = ( R |`s A )
2 subrngsubg 
 |-  ( A e. ( SubRng ` R ) -> A e. ( SubGrp ` R ) )
3 1 subgbas 
 |-  ( A e. ( SubGrp ` R ) -> A = ( Base ` S ) )
4 2 3 syl 
 |-  ( A e. ( SubRng ` R ) -> A = ( Base ` S ) )