Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Rings (extension)
Non-unital rings ("rngs")
ringssrng
Next ⟩
isringrng
Metamath Proof Explorer
Ascii
Unicode
Theorem
ringssrng
Description:
The unital rings are (non-unital) rings.
(Contributed by
AV
, 20-Mar-2020)
Ref
Expression
Assertion
ringssrng
⊢
Ring
⊆
Rng
Proof
Step
Hyp
Ref
Expression
1
ringrng
⊢
x
∈
Ring
→
x
∈
Rng
2
1
ssriv
⊢
Ring
⊆
Rng