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	$$⊢\mathrm{MgmALT}=\left\{m|{+}_m\mathrm{clLaw}{\mathrm{Base}}_m\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmgm2	$$class\mathrm{MgmALT}$$
1		vm	$$setvarm$$
2		cplusg	$$class{+}_{𝑔}$$
3	1	cv	$$setvarm$$
4	3 2	cfv	$$class{+}_m$$
5		ccllaw	$$class\mathrm{clLaw}$$
6		cbs	$$class\mathrm{Base}$$
7	3 6	cfv	$$class{\mathrm{Base}}_m$$
8	4 7 5	wbr	$$wff{+}_m\mathrm{clLaw}{\mathrm{Base}}_m$$
9	8 1	cab	$$class\left\{m|{+}_m\mathrm{clLaw}{\mathrm{Base}}_m\right\}$$
10	0 9	wceq	$$wff\mathrm{MgmALT}=\left\{m|{+}_m\mathrm{clLaw}{\mathrm{Base}}_m\right\}$$