Theorem bj-cmnssmnd

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

	Ref	Expression
Assertion	bj-cmnssmnd	⊢ CMnd ⊆ Mnd

Proof

Step	Hyp	Ref	Expression
1		df-cmn	⊢ CMnd = { 𝑥 ∈ Mnd ∣ ∀ 𝑦 ∈ ( Base ‘ 𝑥 ) ∀ 𝑧 ∈ ( Base ‘ 𝑥 ) ( 𝑦 ( +g ‘ 𝑥 ) 𝑧 ) = ( 𝑧 ( +g ‘ 𝑥 ) 𝑦 ) }
2	1	ssrab3	⊢ CMnd ⊆ Mnd