Metamath Proof Explorer

Theorem mndoisexid

Description: A monoid has an identity element. (Contributed by FL, 2-Nov-2009) (New usage is discouraged.)

		Ref	Expression
	Assertion	mndoisexid	$⊢ G \in MndOp \to G \in ExId$

Step	Hyp	Ref	Expression
1		elinel2	$⊢ G \in (SemiGrp \cap ExId) \to G \in ExId$
2		df-mndo	$⊢ MndOp = SemiGrp \cap ExId$
3	1 2	eleq2s	$⊢ G \in MndOp \to G \in ExId$