Metamath Proof Explorer

Theorem sdrgrcl

Description: Reverse closure for a sub-division-ring predicate. (Contributed by SN, 19-Feb-2025)

Ref Expression
Assertion sdrgrcl 
|- ( A e. ( SubDRing ` R ) -> R e. DivRing )

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 simp1bi 
 |-  ( A e. ( SubDRing ` R ) -> R e. DivRing )