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 e. MndOp -> G e. ExId )

Proof

Step Hyp Ref Expression
1 elinel2 
 |-  ( G e. ( SemiGrp i^i ExId ) -> G e. ExId )
2 df-mndo 
 |-  MndOp = ( SemiGrp i^i ExId )
3 1 2 eleq2s 
 |-  ( G e. MndOp -> G e. ExId )