Theorem bj-cmnssmnd

Description: Commutative monoids are monoids. (Contributed by BJ, 9-Jun-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-cmnssmnd	$$⊢\mathrm{CMnd}\subseteq \mathrm{Mnd}$$

Proof

Step	Hyp	Ref	Expression
1		df-cmn	$$⊢\mathrm{CMnd}=\left\{x\in \mathrm{Mnd}|\forall y\in {\mathrm{Base}}_x\forall z\in {\mathrm{Base}}_{x}y{+}_{x}z=z{+}_{x}y\right\}$$
2	1	ssrab3	$$⊢\mathrm{CMnd}\subseteq \mathrm{Mnd}$$