Theorem bj-modssabl

Description: (The additive groups of) modules are abelian groups. (The elemental version is lmodabl ; see also lmodgrp and lmodcmn .) (Contributed by BJ, 9-Jun-2019)

	Ref	Expression
Assertion	bj-modssabl	⊢ LMod ⊆ Abel

Proof

Step	Hyp	Ref	Expression
1		lmodabl	⊢ ( 𝑥 ∈ LMod → 𝑥 ∈ Abel )
2	1	ssriv	⊢ LMod ⊆ Abel