Definition df-csgrp2

Description: Acommutative semigroup is a semigroup with a commutative operation. (Contributed by AV, 20-Jan-2020)

	Ref	Expression
Assertion	df-csgrp2	⊢ CSGrpALT = { 𝑔 ∈ SGrpALT ∣ ( +g ‘ 𝑔 ) comLaw ( Base ‘ 𝑔 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccsgrp2	⊢ CSGrpALT
1		vg	⊢ 𝑔
2		csgrp2	⊢ SGrpALT
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	⊢ { 𝑔 ∈ SGrpALT ∣ ( +g ‘ 𝑔 ) comLaw ( Base ‘ 𝑔 ) }
11	0 10	wceq	⊢ CSGrpALT = { 𝑔 ∈ SGrpALT ∣ ( +g ‘ 𝑔 ) comLaw ( Base ‘ 𝑔 ) }