Metamath Proof Explorer

Theorem ringssrng

Description: The unital rings are non-unital rings. (Contributed by AV, 20-Mar-2020)

Ref Expression
Assertion ringssrng 
|- Ring C_ Rng

Proof

Step Hyp Ref Expression
1 ringrng 
 |-  ( x e. Ring -> x e. Rng )
2 1 ssriv 
 |-  Ring C_ Rng