Metamath Proof Explorer

Theorem bj-ablssgrp

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

Ref Expression
Assertion bj-ablssgrp 
|- Abel C_ Grp

Proof

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