Definition df-mndo 38576

Description: Obsolete definition, use df-mnd 18825 instead. A monoid is a semigroup with an identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)

Assertion

Ref	Expression
df-mndo	⊢ MndOp = (SemiGrp ∩ ExId )

Detailed syntax breakdown of Definition df-mndo

Step	Hyp	Ref	Expression
1		cmndo 38575	. 2 class MndOp
2		csem 38569	. . 3 class SemiGrp
3		cexid 38553	. . 3 class ExId
4	2, 3	cin 3905	. 2 class (SemiGrp ∩ ExId )
5	1, 4	wceq 1570	1 wff MndOp = (SemiGrp ∩ ExId )

This definition is used by:  mndoissmgrpOLD  38577  mndoisexid  38578  ismndo  38581