Theorem bj-smgrpssmgm

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

	Ref	Expression
Assertion	bj-smgrpssmgm	Could not format assertion : No typesetting found for |- Smgrp C_ Mgm with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-sgrp	Could not format 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 ) ) } : No typesetting found for |- 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 ) ) } with typecode |-
2	1	ssrab3	Could not format Smgrp C_ Mgm : No typesetting found for |- Smgrp C_ Mgm with typecode |-