Theorem mndoisexid

Description: Obsolete theorem, use mndid instead. A monoid has an identity element. (Contributed by FL, 2-Nov-2009) (New usage is discouraged.) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

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