Metamath Proof Explorer


Theorem subrgid

Description: Every ring is a subring of itself. (Contributed by Stefan O'Rear, 30-Nov-2014)

Ref Expression
Hypothesis subrgss.1 B = Base R
Assertion subrgid R Ring B SubRing R

Proof

Step Hyp Ref Expression
1 subrgss.1 B = Base R
2 id R Ring R Ring
3 1 ressid R Ring R 𝑠 B = R
4 3 2 eqeltrd R Ring R 𝑠 B Ring
5 eqid 1 R = 1 R
6 1 5 ringidcl R Ring 1 R B
7 ssid B B
8 6 7 jctil R Ring B B 1 R B
9 1 5 issubrg B SubRing R R Ring R 𝑠 B Ring B B 1 R B
10 2 4 8 9 syl21anbrc R Ring B SubRing R