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

Definition df-sgrOLD 25475
Description: Obsolete version of df-sgrp 16051 as of 3-Feb-2020. A semi-group is an associative magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
Assertion
Ref Expression
df-sgrOLD  |-  SemiGrp  =  (
Magma  i^i  Ass )

Detailed syntax breakdown of Definition df-sgrOLD
StepHypRef Expression
1 csem 25474 . 2  class  SemiGrp
2 cmagm 25462 . . 3  class  Magma
3 cass 25456 . . 3  class  Ass
42, 3cin 3405 . 2  class  ( Magma  i^i 
Ass )
51, 4wceq 1399 1  wff  SemiGrp  =  (
Magma  i^i  Ass )
Colors of variables: wff setvar class
This definition is referenced by:  smgrpismgmOLD  25476  smgrpisass  25477  issmgrpOLD  25478
  Copyright terms: Public domain W3C validator