Metamath Proof Explorer

Theorem bj-cmnssmnd

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

Ref Expression
Assertion bj-cmnssmnd 
|- CMnd C_ Mnd

Proof

Step Hyp Ref Expression
1 df-cmn 
 |-  CMnd = { x e. Mnd | A. y e. ( Base ` x ) A. z e. ( Base ` x ) ( y ( +g ` x ) z ) = ( z ( +g ` x ) y ) }
2 1 ssrab3 
 |-  CMnd C_ Mnd