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

Definition df-mnd 14645
 Description: Definition of a monoid. A monoid is a set equipped with an everywhere defined internal operation (so, a magma, see mndcl 14650), whose operation is associative (so, a semigroup, see mndass 14651) and has a two-sided neutral element (see mndid 14652). (Contributed by Mario Carneiro, 6-Jan-2015.)
Assertion
Ref Expression
df-mnd
Distinct variable group:   ,,,,,,

Detailed syntax breakdown of Definition df-mnd
StepHypRef Expression
1 cmnd 14639 . 2
2 vx . . . . . . . . . . . . 13
32cv 1648 . . . . . . . . . . . 12
4 vy . . . . . . . . . . . . 13
54cv 1648 . . . . . . . . . . . 12
6 vp . . . . . . . . . . . . 13
76cv 1648 . . . . . . . . . . . 12
83, 5, 7co 6040 . . . . . . . . . . 11
9 vb . . . . . . . . . . . 12
109cv 1648 . . . . . . . . . . 11
118, 10wcel 1721 . . . . . . . . . 10
12 vz . . . . . . . . . . . . 13
1312cv 1648 . . . . . . . . . . . 12
148, 13, 7co 6040 . . . . . . . . . . 11
155, 13, 7co 6040 . . . . . . . . . . . 12
163, 15, 7co 6040 . . . . . . . . . . 11
1714, 16wceq 1649 . . . . . . . . . 10
1811, 17wa 359 . . . . . . . . 9
1918, 12, 10wral 2666 . . . . . . . 8
2019, 4, 10wral 2666 . . . . . . 7
2120, 2, 10wral 2666 . . . . . 6
22 ve . . . . . . . . . . . 12
2322cv 1648 . . . . . . . . . . 11
2423, 3, 7co 6040 . . . . . . . . . 10
2524, 3wceq 1649 . . . . . . . . 9
263, 23, 7co 6040 . . . . . . . . . 10
2726, 3wceq 1649 . . . . . . . . 9
2825, 27wa 359 . . . . . . . 8
2928, 2, 10wral 2666 . . . . . . 7
3029, 22, 10wrex 2667 . . . . . 6
3121, 30wa 359 . . . . 5
32 vg . . . . . . 7
3332cv 1648 . . . . . 6
34 cplusg 13484 . . . . . 6
3533, 34cfv 5413 . . . . 5
3631, 6, 35wsbc 3121 . . . 4
37 cbs 13424 . . . . 5
3833, 37cfv 5413 . . . 4
3936, 9, 38wsbc 3121 . . 3
4039, 32cab 2390 . 2
411, 40wceq 1649 1
 Colors of variables: wff set class This definition is referenced by:  ismnd  14647
 Copyright terms: Public domain W3C validator