Metamath Proof Explorer

Theorem bj-grpssmnd

Description: Groups are monoids. (Contributed by BJ, 5-Jan-2024) (Proof modification is discouraged.)

Ref Expression
Assertion bj-grpssmnd 
|- Grp C_ Mnd

Proof

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