MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-sgr Structured version   Unicode version

Definition df-sgr 21911
Description: A semi-group is an associative magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
Assertion
Ref Expression
df-sgr  |-  SemiGrp  =  (
Magma  i^i  Ass )

Detailed syntax breakdown of Definition df-sgr
StepHypRef Expression
1 csem 21910 . 2  class  SemiGrp
2 cmagm 21898 . . 3  class  Magma
3 cass 21892 . . 3  class  Ass
42, 3cin 3311 . 2  class  ( Magma  i^i 
Ass )
51, 4wceq 1652 1  wff  SemiGrp  =  (
Magma  i^i  Ass )
Colors of variables: wff set class
This definition is referenced by:  smgrpismgm  21912  smgrpisass  21913  issmgrp  21914
  Copyright terms: Public domain W3C validator