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

Definition df-cmn 15416
 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 15414 . 2 CMnd
2 va . . . . . . . 8
32cv 1652 . . . . . . 7
4 vb . . . . . . . 8
54cv 1652 . . . . . . 7
6 vg . . . . . . . . 9
76cv 1652 . . . . . . . 8
8 cplusg 13531 . . . . . . . 8
97, 8cfv 5456 . . . . . . 7
103, 5, 9co 6083 . . . . . 6
115, 3, 9co 6083 . . . . . 6
1210, 11wceq 1653 . . . . 5
13 cbs 13471 . . . . . 6
147, 13cfv 5456 . . . . 5
1512, 4, 14wral 2707 . . . 4
1615, 2, 14wral 2707 . . 3
17 cmnd 14686 . . 3
1816, 6, 17crab 2711 . 2
191, 18wceq 1653 1 CMnd
 Colors of variables: wff set class This definition is referenced by:  iscmn  15421
 Copyright terms: Public domain W3C validator