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 | E. t g : ( t X. t ) --> t }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmagm	|- Magma
1		vg	|- g
2		vt	|- t
3	1	cv	|- g
4	2	cv	|- t
5	4 4	cxp	|- ( t X. t )
6	5 4 3	wf	|- g : ( t X. t ) --> t
7	6 2	wex	|- E. t g : ( t X. t ) --> t
8	7 1	cab	|- { g | E. t g : ( t X. t ) --> t }
9	0 8	wceq	|- Magma = { g | E. t g : ( t X. t ) --> t }