Definition df-mndo 38617

Description: Obsolete definition, use df-mnd 18837 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 38616	. 2 class MndOp
2		csem 38610	. . 3 class SemiGrp
3		cexid 38594	. . 3 class ExId
4	2, 3	cin 3898	. 2 class (SemiGrp ∩ ExId )
5	1, 4	wceq 1570	1 wff MndOp = (SemiGrp ∩ ExId )

This definition is used by:  mndoissmgrpOLD  38618  mndoisexid  38619  ismndo  38622