# Metamath Proof Explorer

## 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}}\phantom{\rule{.4em}{0ex}}\forall {b}\in {\mathrm{Base}}_{{g}}\phantom{\rule{.4em}{0ex}}{a}{+}_{{g}}{b}={b}{+}_{{g}}{a}\right\}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 ccmn ${class}\mathrm{CMnd}$
1 vg ${setvar}{g}$
2 cmnd ${class}\mathrm{Mnd}$
3 va ${setvar}{a}$
4 cbs ${class}\mathrm{Base}$
5 1 cv ${setvar}{g}$
6 5 4 cfv ${class}{\mathrm{Base}}_{{g}}$
7 vb ${setvar}{b}$
8 3 cv ${setvar}{a}$
9 cplusg ${class}{+}_{𝑔}$
10 5 9 cfv ${class}{+}_{{g}}$
11 7 cv ${setvar}{b}$
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 ${wff}{a}{+}_{{g}}{b}={b}{+}_{{g}}{a}$
15 14 7 6 wral ${wff}\forall {b}\in {\mathrm{Base}}_{{g}}\phantom{\rule{.4em}{0ex}}{a}{+}_{{g}}{b}={b}{+}_{{g}}{a}$
16 15 3 6 wral ${wff}\forall {a}\in {\mathrm{Base}}_{{g}}\phantom{\rule{.4em}{0ex}}\forall {b}\in {\mathrm{Base}}_{{g}}\phantom{\rule{.4em}{0ex}}{a}{+}_{{g}}{b}={b}{+}_{{g}}{a}$
17 16 1 2 crab ${class}\left\{{g}\in \mathrm{Mnd}|\forall {a}\in {\mathrm{Base}}_{{g}}\phantom{\rule{.4em}{0ex}}\forall {b}\in {\mathrm{Base}}_{{g}}\phantom{\rule{.4em}{0ex}}{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}}\phantom{\rule{.4em}{0ex}}\forall {b}\in {\mathrm{Base}}_{{g}}\phantom{\rule{.4em}{0ex}}{a}{+}_{{g}}{b}={b}{+}_{{g}}{a}\right\}$