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	|- SGrpALT = { g e. MgmALT | ( +g ` g ) assLaw ( Base ` g ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csgrp2	|- SGrpALT
1		vg	|- g
2		cmgm2	|- MgmALT
3		cplusg	|- +g
4	1	cv	|- g
5	4 3	cfv	|- ( +g ` g )
6		casslaw	|- assLaw
7		cbs	|- Base
8	4 7	cfv	|- ( Base ` g )
9	5 8 6	wbr	|- ( +g ` g ) assLaw ( Base ` g )
10	9 1 2	crab	|- { g e. MgmALT | ( +g ` g ) assLaw ( Base ` g ) }
11	0 10	wceq	|- SGrpALT = { g e. MgmALT | ( +g ` g ) assLaw ( Base ` g ) }