Definition df-mgm2

Description: Amagma is a set equipped with a closed operation. Definition 1 of BourbakiAlg1 p. 1, or definition of a groupoid in section I.1 of Bruck p. 1. Note: The term "groupoid" is now widely used to refer to other objects: (small) categories all of whose morphisms are invertible, or groups with a partial function replacing the binary operation. Therefore, we will only use the term "magma" for the present notion in set.mm. (Contributed by AV, 6-Jan-2020)

	Ref	Expression
Assertion	df-mgm2	|- MgmALT = { m | ( +g ` m ) clLaw ( Base ` m ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmgm2	|- MgmALT
1		vm	|- m
2		cplusg	|- +g
3	1	cv	|- m
4	3 2	cfv	|- ( +g ` m )
5		ccllaw	|- clLaw
6		cbs	|- Base
7	3 6	cfv	|- ( Base ` m )
8	4 7 5	wbr	|- ( +g ` m ) clLaw ( Base ` m )
9	8 1	cab	|- { m | ( +g ` m ) clLaw ( Base ` m ) }
10	0 9	wceq	|- MgmALT = { m | ( +g ` m ) clLaw ( Base ` m ) }