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

Definition df-sgr 20998
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 20997 . 2  class  SemiGrp
2 cmagm 20985 . . 3  class  Magma
3 cass 20979 . . 3  class  Ass
42, 3cin 3151 . 2  class  ( Magma  i^i 
Ass )
51, 4wceq 1623 1  wff  SemiGrp  =  (
Magma  i^i  Ass )
Colors of variables: wff set class
This definition is referenced by:  smgrpismgm  20999  smgrpisass  21000  issmgrp  21001
  Copyright terms: Public domain W3C validator