Metamath Proof Explorer


Theorem subrg1cl

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

Ref Expression
Hypothesis subrg1cl.a 1 ˙ = 1 R
Assertion subrg1cl A SubRing R 1 ˙ A

Proof

Step Hyp Ref Expression
1 subrg1cl.a 1 ˙ = 1 R
2 eqid Base R = Base R
3 2 1 issubrg A SubRing R R Ring R 𝑠 A Ring A Base R 1 ˙ A
4 3 simprbi A SubRing R A Base R 1 ˙ A
5 4 simprd A SubRing R 1 ˙ A