This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \cap Ass$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csem	$class SemiGrp$
1		cmagm	$class Magma$
2		cass	$class Ass$
3	1 2	cin	$class (Magma \cap Ass)$
4	0 3	wceq	$wff SemiGrp = Magma \cap Ass$