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

Definition df-submnd 14694
 Description: A submonoid is a subset of a monoid which contains the identity and is closed under the operation. Such subsets are themselves monoids with the same identity. (Contributed by Mario Carneiro, 7-Mar-2015.)
Assertion
Ref Expression
df-submnd SubMnd
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-submnd
StepHypRef Expression
1 csubmnd 14692 . 2 SubMnd
2 vs . . 3
3 cmnd 14639 . . 3
42cv 1648 . . . . . . 7
5 c0g 13678 . . . . . . 7
64, 5cfv 5413 . . . . . 6
7 vt . . . . . . 7
87cv 1648 . . . . . 6
96, 8wcel 1721 . . . . 5
10 vx . . . . . . . . . 10
1110cv 1648 . . . . . . . . 9
12 vy . . . . . . . . . 10
1312cv 1648 . . . . . . . . 9
14 cplusg 13484 . . . . . . . . . 10
154, 14cfv 5413 . . . . . . . . 9
1611, 13, 15co 6040 . . . . . . . 8
1716, 8wcel 1721 . . . . . . 7
1817, 12, 8wral 2666 . . . . . 6
1918, 10, 8wral 2666 . . . . 5
209, 19wa 359 . . . 4
21 cbs 13424 . . . . . 6
224, 21cfv 5413 . . . . 5
2322cpw 3759 . . . 4
2420, 7, 23crab 2670 . . 3
252, 3, 24cmpt 4226 . 2
261, 25wceq 1649 1 SubMnd
 Colors of variables: wff set class This definition is referenced by:  submrcl  14702  issubm  14703
 Copyright terms: Public domain W3C validator