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 ∩ Ass )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csem	⊢ SemiGrp
1		cmagm	⊢ Magma
2		cass	⊢ Ass
3	1 2	cin	⊢ ( Magma ∩ Ass )
4	0 3	wceq	⊢ SemiGrp = ( Magma ∩ Ass )