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

Metamath Proof Explorer

Definition df-mgmOLD

Description: Obsolete version of df-mgm as of 3-Feb-2020. A magma is a binary internal operation. (Contributed by FL, 2-Nov-2009) (New usage is discouraged.)

		Ref	Expression
	Assertion	df-mgmOLD	$⊢ Magma = \{g \| \exists t g : t \times t ⟶ t\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmagm	$class Magma$
1		vg	$setvar g$
2		vt	$setvar t$
3	1	cv	$setvar g$
4	2	cv	$setvar t$
5	4 4	cxp	$class (t \times t)$
6	5 4 3	wf	$wff g : t \times t ⟶ t$
7	6 2	wex	$wff \exists t g : t \times t ⟶ t$
8	7 1	cab	$class \{g \| \exists t g : t \times t ⟶ t\}$
9	0 8	wceq	$wff Magma = \{g \| \exists t g : t \times t ⟶ t\}$