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	$$⊢\mathrm{LMod}\subseteq \mathrm{Abel}$$

Proof

Step	Hyp	Ref	Expression
1		lmodabl	$$⊢x\in \mathrm{LMod}\to x\in \mathrm{Abel}$$
2	1	ssriv	$$⊢\mathrm{LMod}\subseteq \mathrm{Abel}$$