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