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

Definition df-cmn 15369
 Description: Define class of all commutative monoids. (Contributed by Mario Carneiro, 6-Jan-2015.)
Assertion
Ref Expression
df-cmn CMnd
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-cmn
StepHypRef Expression
1 ccmn 15367 . 2 CMnd
2 va . . . . . . . 8
32cv 1648 . . . . . . 7
4 vb . . . . . . . 8
54cv 1648 . . . . . . 7
6 vg . . . . . . . . 9
76cv 1648 . . . . . . . 8
8 cplusg 13484 . . . . . . . 8
97, 8cfv 5413 . . . . . . 7
103, 5, 9co 6040 . . . . . 6
115, 3, 9co 6040 . . . . . 6
1210, 11wceq 1649 . . . . 5
13 cbs 13424 . . . . . 6
147, 13cfv 5413 . . . . 5
1512, 4, 14wral 2666 . . . 4
1615, 2, 14wral 2666 . . 3
17 cmnd 14639 . . 3
1816, 6, 17crab 2670 . 2
191, 18wceq 1649 1 CMnd
 Colors of variables: wff set class This definition is referenced by:  iscmn  15374
 Copyright terms: Public domain W3C validator