Metamath Proof Explorer

Theorem bj-ablsscmn

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

Ref Expression
Assertion bj-ablsscmn 
|- Abel C_ CMnd

Proof

Step Hyp Ref Expression
1 df-abl 
 |-  Abel = ( Grp i^i CMnd )
2 inss2 
 |-  ( Grp i^i CMnd ) C_ CMnd
3 1 2 eqsstri 
 |-  Abel C_ CMnd