Metamath Proof Explorer

Theorem subrngrcl

Description: Reverse closure for a subring predicate. (Contributed by AV, 14-Feb-2025)

Ref Expression
Assertion subrngrcl 
|- ( A e. ( SubRng ` R ) -> R e. Rng )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` R ) = ( Base ` R )
2 1 issubrng 
 |-  ( A e. ( SubRng ` R ) <-> ( R e. Rng /\ ( R |`s A ) e. Rng /\ A C_ ( Base ` R ) ) )
3 2 simp1bi 
 |-  ( A e. ( SubRng ` R ) -> R e. Rng )