Description: Obsolete version of mndsgrp as of 3-Feb-2020. A monoid is a semigroup. (Contributed by FL, 2-Nov-2009) (New usage is discouraged.) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | mndoissmgrpOLD | |- ( G e. MndOp -> G e. SemiGrp ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elin | |- ( G e. ( SemiGrp i^i ExId ) <-> ( G e. SemiGrp /\ G e. ExId ) ) |
|
| 2 | 1 | simplbi | |- ( G e. ( SemiGrp i^i ExId ) -> G e. SemiGrp ) |
| 3 | df-mndo | |- MndOp = ( SemiGrp i^i ExId ) |
|
| 4 | 2 3 | eleq2s | |- ( G e. MndOp -> G e. SemiGrp ) |