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 ‘ 𝑚 ) }