Metamath Proof Explorer


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 MgmALT | + m comLaw Base m

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccmgm2 class CMgmALT
1 vm setvar m
2 cmgm2 class MgmALT
3 cplusg class + 𝑔
4 1 cv setvar m
5 4 3 cfv class + m
6 ccomlaw class comLaw
7 cbs class Base
8 4 7 cfv class Base m
9 5 8 6 wbr wff + m comLaw Base m
10 9 1 2 crab class m MgmALT | + m comLaw Base m
11 0 10 wceq wff CMgmALT = m MgmALT | + m comLaw Base m