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 ) )