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	$$⊢\mathrm{MndOp}=\mathrm{SemiGrp}\cap \mathrm{ExId}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmndo	$$class\mathrm{MndOp}$$
1		csem	$$class\mathrm{SemiGrp}$$
2		cexid	$$class\mathrm{ExId}$$
3	1 2	cin	$$class\left(\mathrm{SemiGrp}\cap \mathrm{ExId}\right)$$
4	0 3	wceq	$$wff\mathrm{MndOp}=\mathrm{SemiGrp}\cap \mathrm{ExId}$$