Definition df-cmn

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

	Ref	Expression
Assertion	df-cmn	$$⊢\mathrm{CMnd}=\left\{g\in \mathrm{Mnd}|\forall a\in {\mathrm{Base}}_g\forall b\in {\mathrm{Base}}_{g}a{+}_{g}b=b{+}_{g}a\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccmn	$$class\mathrm{CMnd}$$
1		vg	$$setvarg$$
2		cmnd	$$class\mathrm{Mnd}$$
3		va	$$setvara$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarg$$
6	5 4	cfv	$$class{\mathrm{Base}}_g$$
7		vb	$$setvarb$$
8	3	cv	$$setvara$$
9		cplusg	$$class{+}_{𝑔}$$
10	5 9	cfv	$$class{+}_g$$
11	7	cv	$$setvarb$$
12	8 11 10	co	$$class\left(a{+}_{g}b\right)$$
13	11 8 10	co	$$class\left(b{+}_{g}a\right)$$
14	12 13	wceq	$$wffa{+}_{g}b=b{+}_{g}a$$
15	14 7 6	wral	$$wff\forall b\in {\mathrm{Base}}_{g}a{+}_{g}b=b{+}_{g}a$$
16	15 3 6	wral	$$wff\forall a\in {\mathrm{Base}}_g\forall b\in {\mathrm{Base}}_{g}a{+}_{g}b=b{+}_{g}a$$
17	16 1 2	crab	$$class\left\{g\in \mathrm{Mnd}|\forall a\in {\mathrm{Base}}_g\forall b\in {\mathrm{Base}}_{g}a{+}_{g}b=b{+}_{g}a\right\}$$
18	0 17	wceq	$$wff\mathrm{CMnd}=\left\{g\in \mathrm{Mnd}|\forall a\in {\mathrm{Base}}_g\forall b\in {\mathrm{Base}}_{g}a{+}_{g}b=b{+}_{g}a\right\}$$