Theorem bj-smgrpssmgm

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

	Ref	Expression
Assertion	bj-smgrpssmgm	$$⊢\mathrm{Smgrp}\subseteq \mathrm{Mgm}$$

Proof

Step	Hyp	Ref	Expression
1		df-sgrp	$$⊢\mathrm{Smgrp}=\left\{g\in \mathrm{Mgm}|\underset{\dot{}}{[}{\mathrm{Base}}_g/b\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_g/p\underset{\dot{}}{]}\forall x\in b\forall y\in b\forall z\in b\left(xpy\right)pz=xp\left(ypz\right)\right\}$$
2	1	ssrab3	$$⊢\mathrm{Smgrp}\subseteq \mathrm{Mgm}$$