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

Detailed syntax breakdown

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