Definition df-mndo 25467

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

Assertion

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

Detailed syntax breakdown of Definition df-mndo

Step	Hyp	Ref	Expression
1		cmndo 25466	. 2 class MndOp
2		csem 25459	. . 3 class SemiGrp
3		cexid 25443	. . 3 class ExId
4	2, 3	cin 3470	. 2 class ( SemiGrp i^i ExId )
5	1, 4	wceq 1395	1 wff MndOp = ( SemiGrp i^i ExId )

This definition is referenced by:  mndoissmgrpOLD  25468  mndoisexid  25469  ismndo  25472