Definition df-cmgm2

Description: Acommutative magma is a magma with a commutative operation. Definition 8 of BourbakiAlg1 p. 7. (Contributed by AV, 20-Jan-2020)

	Ref	Expression
Assertion	df-cmgm2	|- CMgmALT = { m e. MgmALT | ( +g ` m ) comLaw ( Base ` m ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccmgm2	|- CMgmALT
1		vm	|- m
2		cmgm2	|- MgmALT
3		cplusg	|- +g
4	1	cv	|- m
5	4 3	cfv	|- ( +g ` m )
6		ccomlaw	|- comLaw
7		cbs	|- Base
8	4 7	cfv	|- ( Base ` m )
9	5 8 6	wbr	|- ( +g ` m ) comLaw ( Base ` m )
10	9 1 2	crab	|- { m e. MgmALT | ( +g ` m ) comLaw ( Base ` m ) }
11	0 10	wceq	|- CMgmALT = { m e. MgmALT | ( +g ` m ) comLaw ( Base ` m ) }