Metamath Proof Explorer

Theorem sdrgsubrg

Description: A sub-division-ring is a subring. (Contributed by SN, 19-Feb-2025)

Ref Expression
Assertion sdrgsubrg 
|- ( A e. ( SubDRing ` R ) -> A e. ( SubRing ` R ) )

Proof

Step Hyp Ref Expression
1 issdrg 
 |-  ( A e. ( SubDRing ` R ) <-> ( R e. DivRing /\ A e. ( SubRing ` R ) /\ ( R |`s A ) e. DivRing ) )
2 1 simp2bi 
 |-  ( A e. ( SubDRing ` R ) -> A e. ( SubRing ` R ) )