Metamath Proof Explorer


Definition df-sgrp2

Description: Asemigroup is a magma with an associative operation. Definition in section II.1 of Bruck p. 23, or of an "associative magma" in definition 5 of BourbakiAlg1 p. 4, or of a semigroup in section 1.3 of Hall p. 7. (Contributed by AV, 6-Jan-2020)

Ref Expression
Assertion df-sgrp2 SGrpALT = g MgmALT | + g assLaw Base g

Detailed syntax breakdown

Step Hyp Ref Expression
0 csgrp2 class SGrpALT
1 vg setvar g
2 cmgm2 class MgmALT
3 cplusg class + 𝑔
4 1 cv setvar g
5 4 3 cfv class + g
6 casslaw class assLaw
7 cbs class Base
8 4 7 cfv class Base g
9 5 8 6 wbr wff + g assLaw Base g
10 9 1 2 crab class g MgmALT | + g assLaw Base g
11 0 10 wceq wff SGrpALT = g MgmALT | + g assLaw Base g