Theorem subrgss

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

	Ref	Expression
Hypothesis	subrgss.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion	subrgss	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 ⊆ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		subrgss.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
3	1 2	issubrg	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ↔ ( ( 𝑅 ∈ Ring ∧ ( 𝑅 ↾s 𝐴 ) ∈ Ring ) ∧ ( 𝐴 ⊆ 𝐵 ∧ ( 1r ‘ 𝑅 ) ∈ 𝐴 ) ) )
4	3	simprbi	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( 𝐴 ⊆ 𝐵 ∧ ( 1r ‘ 𝑅 ) ∈ 𝐴 ) )
5	4	simpld	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 ⊆ 𝐵 )