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 = { g e. SGrpALT | ( +g ` g ) comLaw ( Base ` g ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccsgrp2	|- CSGrpALT
1		vg	|- g
2		csgrp2	|- SGrpALT
3		cplusg	|- +g
4	1	cv	|- g
5	4 3	cfv	|- ( +g ` g )
6		ccomlaw	|- comLaw
7		cbs	|- Base
8	4 7	cfv	|- ( Base ` g )
9	5 8 6	wbr	|- ( +g ` g ) comLaw ( Base ` g )
10	9 1 2	crab	|- { g e. SGrpALT | ( +g ` g ) comLaw ( Base ` g ) }
11	0 10	wceq	|- CSGrpALT = { g e. SGrpALT | ( +g ` g ) comLaw ( Base ` g ) }