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

Definition df-sgr 21014
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 21013 . 2  class  SemiGrp
2 cmagm 21001 . . 3  class  Magma
3 cass 20995 . . 3  class  Ass
42, 3cin 3164 . 2  class  ( Magma  i^i 
Ass )
51, 4wceq 1632 1  wff  SemiGrp  =  (
Magma  i^i  Ass )
Colors of variables: wff set class
This definition is referenced by:  smgrpismgm  21015  smgrpisass  21016  issmgrp  21017
  Copyright terms: Public domain W3C validator