Definition df-sgr 10378

Description: A semi-group is an associative magma.

Assertion

Ref	Expression
df-sgr	|- SemiGrp = (Magma i^i Ass)

Detailed syntax breakdown of Definition df-sgr

Step	Hyp	Ref	Expression
1		csem 10377	. 2 class SemiGrp
2		cmagm 10365	. . 3 class Magma
3		cass 10359	. . 3 class Ass
4	2, 3	cin 2592	. 2 class (Magma i^i Ass)
5	1, 4	wceq 1298	1 wff SemiGrp = (Magma i^i Ass)

This definition is referenced by:  smgrpismgm 10379  smgrpisass 10380  issmgrp 10381

Copyright terms: Public domain