Metamath Proof Explorer

Theorem subrgrcl

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

Ref Expression
Assertion subrgrcl 
|- ( A e. ( SubRing ` R ) -> R e. Ring )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` R ) = ( Base ` R )
2 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
3 1 2 issubrg 
 |-  ( A e. ( SubRing ` R ) <-> ( ( R e. Ring /\ ( R |`s A ) e. Ring ) /\ ( A C_ ( Base ` R ) /\ ( 1r ` R ) e. A ) ) )
4 3 simplbi 
 |-  ( A e. ( SubRing ` R ) -> ( R e. Ring /\ ( R |`s A ) e. Ring ) )
5 4 simpld 
 |-  ( A e. ( SubRing ` R ) -> R e. Ring )