Metamath Proof Explorer


Theorem subrngrng

Description: A subring is a non-unital ring. (Contributed by AV, 14-Feb-2025)

Ref Expression
Hypothesis subrngrng.1 S = R 𝑠 A
Assertion subrngrng A SubRng R S Rng

Proof

Step Hyp Ref Expression
1 subrngrng.1 S = R 𝑠 A
2 simp2 R Rng R 𝑠 A Rng A Base R R 𝑠 A Rng
3 eqid Base R = Base R
4 3 issubrng A SubRng R R Rng R 𝑠 A Rng A Base R
5 1 eleq1i S Rng R 𝑠 A Rng
6 2 4 5 3imtr4i A SubRng R S Rng