Theorem mndomgmid

Description: A monoid is a magma with an identity element. (Contributed by FL, 18-Feb-2010) (New usage is discouraged.)

	Ref	Expression
Assertion	mndomgmid	⊢ ( 𝐺 ∈ MndOp → 𝐺 ∈ ( Magma ∩ ExId ) )

Proof

Step	Hyp	Ref	Expression
1		mndoismgmOLD	⊢ ( 𝐺 ∈ MndOp → 𝐺 ∈ Magma )
2		mndoisexid	⊢ ( 𝐺 ∈ MndOp → 𝐺 ∈ ExId )
3	1 2	elind	⊢ ( 𝐺 ∈ MndOp → 𝐺 ∈ ( Magma ∩ ExId ) )