Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Rings (extension)
Non-unital rings ("rngs")
ringssrng
Next ⟩
isringrng
Metamath Proof Explorer
Ascii
Structured
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
⊢
(
𝑥
∈ Ring →
𝑥
∈ Rng )
2
1
ssriv
⊢
Ring ⊆ Rng