Metamath Proof Explorer

Definition df-mndo

Description: A monoid is a semigroup with an identity element. (Contributed by FL, 2-Nov-2009) (New usage is discouraged.)

Ref Expression
Assertion df-mndo 
|- MndOp = ( SemiGrp i^i ExId )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmndo 
 |-  MndOp
1 csem 
 |-  SemiGrp
2 cexid 
 |-  ExId
3 1 2 cin 
 |-  ( SemiGrp i^i ExId )
4 0 3 wceq 
 |-  MndOp = ( SemiGrp i^i ExId )