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 )