MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cmn Structured version   Visualization version   GIF version

Definition df-cmn 17960
Description: Define class of all commutative monoids. (Contributed by Mario Carneiro, 6-Jan-2015.)
Assertion
Ref Expression
df-cmn CMnd = {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)(𝑎(+g𝑔)𝑏) = (𝑏(+g𝑔)𝑎)}
Distinct variable group:   𝑎,𝑏,𝑔

Detailed syntax breakdown of Definition df-cmn
StepHypRef Expression
1 ccmn 17958 . 2 class CMnd
2 va . . . . . . . 8 setvar 𝑎
32cv 1473 . . . . . . 7 class 𝑎
4 vb . . . . . . . 8 setvar 𝑏
54cv 1473 . . . . . . 7 class 𝑏
6 vg . . . . . . . . 9 setvar 𝑔
76cv 1473 . . . . . . . 8 class 𝑔
8 cplusg 15710 . . . . . . . 8 class +g
97, 8cfv 5786 . . . . . . 7 class (+g𝑔)
103, 5, 9co 6523 . . . . . 6 class (𝑎(+g𝑔)𝑏)
115, 3, 9co 6523 . . . . . 6 class (𝑏(+g𝑔)𝑎)
1210, 11wceq 1474 . . . . 5 wff (𝑎(+g𝑔)𝑏) = (𝑏(+g𝑔)𝑎)
13 cbs 15637 . . . . . 6 class Base
147, 13cfv 5786 . . . . 5 class (Base‘𝑔)
1512, 4, 14wral 2891 . . . 4 wff 𝑏 ∈ (Base‘𝑔)(𝑎(+g𝑔)𝑏) = (𝑏(+g𝑔)𝑎)
1615, 2, 14wral 2891 . . 3 wff 𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)(𝑎(+g𝑔)𝑏) = (𝑏(+g𝑔)𝑎)
17 cmnd 17059 . . 3 class Mnd
1816, 6, 17crab 2895 . 2 class {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)(𝑎(+g𝑔)𝑏) = (𝑏(+g𝑔)𝑎)}
191, 18wceq 1474 1 wff CMnd = {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)(𝑎(+g𝑔)𝑏) = (𝑏(+g𝑔)𝑎)}
Colors of variables: wff setvar class
This definition is referenced by:  iscmn  17965  bj-cmnssmnd  32112
  Copyright terms: Public domain W3C validator