Theorem subrg1cl

Description: A subring contains the multiplicative identity. (Contributed by Stefan O'Rear, 27-Nov-2014)

	Ref	Expression
Hypothesis	subrg1cl.a	|- .1. = ( 1r ` R )
Assertion	subrg1cl	|- ( A e. ( SubRing ` R ) -> .1. e. A )

Proof

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