Theorem sdrgss

Description: A division subring is a subset of the base set. (Contributed by Thierry Arnoux, 21-Aug-2023)

	Ref	Expression
Hypothesis	sdrgid.1	|- B = ( Base ` R )
Assertion	sdrgss	|- ( S e. ( SubDRing ` R ) -> S C_ B )

Proof

Step	Hyp	Ref	Expression
1		sdrgid.1	|- B = ( Base ` R )
2		issdrg	|- ( S e. ( SubDRing ` R ) <-> ( R e. DivRing /\ S e. ( SubRing ` R ) /\ ( R |`s S ) e. DivRing ) )
3	1	subrgss	|- ( S e. ( SubRing ` R ) -> S C_ B )
4	3	3ad2ant2	|- ( ( R e. DivRing /\ S e. ( SubRing ` R ) /\ ( R |`s S ) e. DivRing ) -> S C_ B )
5	2 4	sylbi	|- ( S e. ( SubDRing ` R ) -> S C_ B )