This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

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