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 ) |
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 ) |