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

Definition df-submnd 14731
 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 14729 . 2 SubMnd
2 vs . . 3
3 cmnd 14676 . . 3
42cv 1651 . . . . . . 7
5 c0g 13715 . . . . . . 7
64, 5cfv 5446 . . . . . 6
7 vt . . . . . . 7
87cv 1651 . . . . . 6
96, 8wcel 1725 . . . . 5
10 vx . . . . . . . . . 10
1110cv 1651 . . . . . . . . 9
12 vy . . . . . . . . . 10
1312cv 1651 . . . . . . . . 9
14 cplusg 13521 . . . . . . . . . 10
154, 14cfv 5446 . . . . . . . . 9
1611, 13, 15co 6073 . . . . . . . 8
1716, 8wcel 1725 . . . . . . 7
1817, 12, 8wral 2697 . . . . . 6
1918, 10, 8wral 2697 . . . . 5
209, 19wa 359 . . . 4
21 cbs 13461 . . . . . 6
224, 21cfv 5446 . . . . 5
2322cpw 3791 . . . 4
2420, 7, 23crab 2701 . . 3
252, 3, 24cmpt 4258 . 2
261, 25wceq 1652 1 SubMnd
 Colors of variables: wff set class This definition is referenced by:  submrcl  14739  issubm  14740
 Copyright terms: Public domain W3C validator