Metamath Proof Explorer


Theorem subrgrcl

Description: Reverse closure for a subring predicate. (Contributed by Mario Carneiro, 3-Dec-2014)

Ref Expression
Assertion subrgrcl A SubRing R R Ring

Proof

Step Hyp Ref Expression
1 eqid Base R = Base R
2 eqid 1 R = 1 R
3 1 2 issubrg A SubRing R R Ring R 𝑠 A Ring A Base R 1 R A
4 3 simplbi A SubRing R R Ring R 𝑠 A Ring
5 4 simpld A SubRing R R Ring