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 = ( Magma i^i Ass )

Detailed syntax breakdown


 |-  SemiGrp
 |-  Magma
 |-  Ass
 |-  ( Magma i^i Ass )
 |-  SemiGrp = ( Magma i^i Ass )

Step	Hyp	Ref	Expression
0		csem	\|- SemiGrp
1		cmagm	\|- Magma
2		cass	\|- Ass
3	1 2	cin	\|- ( Magma i^i Ass )
4	0 3	wceq	\|- SemiGrp = ( Magma i^i Ass )