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

Definition df-mnd 14691
 Description: Definition of a monoid. A monoid is a set equipped with an everywhere defined internal operation (so, a magma, see mndcl 14696), whose operation is associative (so, a semigroup, see mndass 14697) and has a two-sided neutral element (see mndid 14698). (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 14685 . 2
2 vx . . . . . . . . . . . . 13
32cv 1652 . . . . . . . . . . . 12
4 vy . . . . . . . . . . . . 13
54cv 1652 . . . . . . . . . . . 12
6 vp . . . . . . . . . . . . 13
76cv 1652 . . . . . . . . . . . 12
83, 5, 7co 6082 . . . . . . . . . . 11
9 vb . . . . . . . . . . . 12
109cv 1652 . . . . . . . . . . 11
118, 10wcel 1726 . . . . . . . . . 10
12 vz . . . . . . . . . . . . 13
1312cv 1652 . . . . . . . . . . . 12
148, 13, 7co 6082 . . . . . . . . . . 11
155, 13, 7co 6082 . . . . . . . . . . . 12
163, 15, 7co 6082 . . . . . . . . . . 11
1714, 16wceq 1653 . . . . . . . . . 10
1811, 17wa 360 . . . . . . . . 9
1918, 12, 10wral 2706 . . . . . . . 8
2019, 4, 10wral 2706 . . . . . . 7
2120, 2, 10wral 2706 . . . . . 6
22 ve . . . . . . . . . . . 12
2322cv 1652 . . . . . . . . . . 11
2423, 3, 7co 6082 . . . . . . . . . 10
2524, 3wceq 1653 . . . . . . . . 9
263, 23, 7co 6082 . . . . . . . . . 10
2726, 3wceq 1653 . . . . . . . . 9
2825, 27wa 360 . . . . . . . 8
2928, 2, 10wral 2706 . . . . . . 7
3029, 22, 10wrex 2707 . . . . . 6
3121, 30wa 360 . . . . 5
32 vg . . . . . . 7
3332cv 1652 . . . . . 6
34 cplusg 13530 . . . . . 6
3533, 34cfv 5455 . . . . 5
3631, 6, 35wsbc 3162 . . . 4
37 cbs 13470 . . . . 5
3833, 37cfv 5455 . . . 4
3936, 9, 38wsbc 3162 . . 3
4039, 32cab 2423 . 2
411, 40wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  ismnd  14693
 Copyright terms: Public domain W3C validator