Metamath Proof Explorer

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 
|- ( G e. MndOp -> G e. ( Magma i^i ExId ) )

Proof

Step Hyp Ref Expression
1 mndoismgmOLD 
 |-  ( G e. MndOp -> G e. Magma )
2 mndoisexid 
 |-  ( G e. MndOp -> G e. ExId )
3 1 2 elind 
 |-  ( G e. MndOp -> G e. ( Magma i^i ExId ) )