Theorem subrgss

Description: A subring is a subset. (Contributed by Stefan O'Rear, 27-Nov-2014)

	Ref	Expression
Hypothesis	subrgss.1	|- B = ( Base ` R )
Assertion	subrgss	|- ( A e. ( SubRing ` R ) -> A C_ B )

Proof

Step	Hyp	Ref	Expression
1		subrgss.1	|- B = ( 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_ B /\ ( 1r ` R ) e. A ) ) )
4	3	simprbi	|- ( A e. ( SubRing ` R ) -> ( A C_ B /\ ( 1r ` R ) e. A ) )
5	4	simpld	|- ( A e. ( SubRing ` R ) -> A C_ B )