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 = { 𝑚 ∈ MgmALT ∣ ( +g𝑚 ) comLaw ( Base ‘ 𝑚 ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccmgm2 CMgmALT
1 vm 𝑚
2 cmgm2 MgmALT
3 cplusg +g
4 1 cv 𝑚
5 4 3 cfv ( +g𝑚 )
6 ccomlaw comLaw
7 cbs Base
8 4 7 cfv ( Base ‘ 𝑚 )
9 5 8 6 wbr ( +g𝑚 ) comLaw ( Base ‘ 𝑚 )
10 9 1 2 crab { 𝑚 ∈ MgmALT ∣ ( +g𝑚 ) comLaw ( Base ‘ 𝑚 ) }
11 0 10 wceq CMgmALT = { 𝑚 ∈ MgmALT ∣ ( +g𝑚 ) comLaw ( Base ‘ 𝑚 ) }