Metamath Proof Explorer

Theorem bj-smgrpssmgm

Description: Semigroups are magmas. (Contributed by BJ, 12-Apr-2024) (Proof modification is discouraged.)

Ref Expression
Assertion bj-smgrpssmgm 
|- Smgrp C_ Mgm

Proof

Step Hyp Ref Expression
1 df-sgrp 
 |-  Smgrp = { g e. Mgm | [. ( Base ` g ) / b ]. [. ( +g ` g ) / p ]. A. x e. b A. y e. b A. z e. b ( ( x p y ) p z ) = ( x p ( y p z ) ) }
2 1 ssrab3 
 |-  Smgrp C_ Mgm