Definition df-sgrp2

Description: Asemigroup is a magma with an associative operation. Definition in section II.1 of Bruck p. 23, or of an "associative magma" in definition 5 of BourbakiAlg1 p. 4, or of a semigroup in section 1.3 of Hall p. 7. (Contributed by AV, 6-Jan-2020)

	Ref	Expression
Assertion	df-sgrp2	$$⊢\mathrm{SGrpALT}=\left\{g\in \mathrm{MgmALT}|{+}_g\mathrm{assLaw}{\mathrm{Base}}_g\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csgrp2	$$class\mathrm{SGrpALT}$$
1		vg	$$setvarg$$
2		cmgm2	$$class\mathrm{MgmALT}$$
3		cplusg	$$class{+}_{𝑔}$$
4	1	cv	$$setvarg$$
5	4 3	cfv	$$class{+}_g$$
6		casslaw	$$class\mathrm{assLaw}$$
7		cbs	$$class\mathrm{Base}$$
8	4 7	cfv	$$class{\mathrm{Base}}_g$$
9	5 8 6	wbr	$$wff{+}_g\mathrm{assLaw}{\mathrm{Base}}_g$$
10	9 1 2	crab	$$class\left\{g\in \mathrm{MgmALT}|{+}_g\mathrm{assLaw}{\mathrm{Base}}_g\right\}$$
11	0 10	wceq	$$wff\mathrm{SGrpALT}=\left\{g\in \mathrm{MgmALT}|{+}_g\mathrm{assLaw}{\mathrm{Base}}_g\right\}$$