Metamath Proof Explorer


Definition df-sgrOLD

Description: Obsolete version of df-sgrp as of 3-Feb-2020. A semigroup is an associative magma. (Contributed by FL, 2-Nov-2009) (New usage is discouraged.)

Ref Expression
Assertion df-sgrOLD SemiGrp=MagmaAss

Detailed syntax breakdown

Step Hyp Ref Expression
0 csem classSemiGrp
1 cmagm classMagma
2 cass classAss
3 1 2 cin classMagmaAss
4 0 3 wceq wffSemiGrp=MagmaAss