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=mMgmALT|+mcomLawBasem

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccmgm2 classCMgmALT
1 vm setvarm
2 cmgm2 classMgmALT
3 cplusg class+𝑔
4 1 cv setvarm
5 4 3 cfv class+m
6 ccomlaw classcomLaw
7 cbs classBase
8 4 7 cfv classBasem
9 5 8 6 wbr wff+mcomLawBasem
10 9 1 2 crab classmMgmALT|+mcomLawBasem
11 0 10 wceq wffCMgmALT=mMgmALT|+mcomLawBasem