Definition df-mgmOLD 33648

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

Assertion

Ref	Expression
df-mgmOLD	|- Magma = { g | E. t g : ( t X. t ) --> t }

Distinct variable group:   t, g

Detailed syntax breakdown of Definition df-mgmOLD

Step	Hyp	Ref	Expression
1		cmagm 33647	. 2 class Magma
2		vt	. . . . . . 7 setvar t
3	2	cv 1482	. . . . . 6 class t
4	3, 3	cxp 5112	. . . . 5 class ( t X. t )
5		vg	. . . . . 6 setvar g
6	5	cv 1482	. . . . 5 class g
7	4, 3, 6	wf 5884	. . . 4 wff g : ( t X. t ) --> t
8	7, 2	wex 1704	. . 3 wff E. t g : ( t X. t ) --> t
9	8, 5	cab 2608	. 2 class { g | E. t g : ( t X. t ) --> t }
10	1, 9	wceq 1483	1 wff Magma = { g | E. t g : ( t X. t ) --> t }

This definition is referenced by:  ismgmOLD  33649