Definition df-mndo

Description: Obsolete definition, use df-mnd instead. 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 ∩ ExId )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmndo	⊢ MndOp
1		csem	⊢ SemiGrp
2		cexid	⊢ ExId
3	1 2	cin	⊢ ( SemiGrp ∩ ExId )
4	0 3	wceq	⊢ MndOp = ( SemiGrp ∩ ExId )