Theorem mndoisexid

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

	Ref	Expression
Assertion	mndoisexid	⊢ ( 𝐺 ∈ MndOp → 𝐺 ∈ ExId )

Proof

Step	Hyp	Ref	Expression
1		elinel2	⊢ ( 𝐺 ∈ ( SemiGrp ∩ ExId ) → 𝐺 ∈ ExId )
2		df-mndo	⊢ MndOp = ( SemiGrp ∩ ExId )
3	1 2	eleq2s	⊢ ( 𝐺 ∈ MndOp → 𝐺 ∈ ExId )