Definition df-cmn 13823

Description: Define class of all commutative monoids. (Contributed by Mario Carneiro, 6-Jan-2015.)

Assertion

Ref	Expression
df-cmn	|- CMnd = { g e. Mnd | A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( a ( +g ` g ) b ) = ( b ( +g ` g ) a ) }

Distinct variable group:   a, b, g

Detailed syntax breakdown of Definition df-cmn

Step	Hyp	Ref	Expression
1		ccmn 13821	. 2 class CMnd
2		va	. . . . . . . 8 setvar a
3	2	cv 1394	. . . . . . 7 class a
4		vb	. . . . . . . 8 setvar b
5	4	cv 1394	. . . . . . 7 class b
6		vg	. . . . . . . . 9 setvar g
7	6	cv 1394	. . . . . . . 8 class g
8		cplusg 13110	. . . . . . . 8 class +g
9	7, 8	cfv 5318	. . . . . . 7 class ( +g ` g )
10	3, 5, 9	co 6001	. . . . . 6 class ( a ( +g ` g ) b )
11	5, 3, 9	co 6001	. . . . . 6 class ( b ( +g ` g ) a )
12	10, 11	wceq 1395	. . . . 5 wff ( a ( +g ` g ) b ) = ( b ( +g ` g ) a )
13		cbs 13032	. . . . . 6 class Base
14	7, 13	cfv 5318	. . . . 5 class ( Base ` g )
15	12, 4, 14	wral 2508	. . . 4 wff A. b e. ( Base ` g ) ( a ( +g ` g ) b ) = ( b ( +g ` g ) a )
16	15, 2, 14	wral 2508	. . 3 wff A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( a ( +g ` g ) b ) = ( b ( +g ` g ) a )
17		cmnd 13449	. . 3 class Mnd
18	16, 6, 17	crab 2512	. 2 class { g e. Mnd | A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( a ( +g ` g ) b ) = ( b ( +g ` g ) a ) }
19	1, 18	wceq 1395	1 wff CMnd = { g e. Mnd | A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( a ( +g ` g ) b ) = ( b ( +g ` g ) a ) }

This definition is referenced by:  iscmn  13830