Metamath Proof Explorer


Theorem subrngrcl

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

Ref Expression
Assertion subrngrcl A SubRng R R Rng

Proof

Step Hyp Ref Expression
1 eqid Base R = Base R
2 1 issubrng A SubRng R R Rng R 𝑠 A Rng A Base R
3 2 simp1bi A SubRng R R Rng