Definition df-mgm 10366

Description: A magma is a binary internal operation.

Assertion

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

Distinct variable group:   t,g

Detailed syntax breakdown of Definition df-mgm

Step	Hyp	Ref	Expression
1		cmagm 10365	. 2 class Magma
2		vt	. . . . . . 7 set t
3	2	cv 1297	. . . . . 6 class t
4	3, 3	cxp 3984	. . . . 5 class (t X. t)
5		vg	. . . . . 6 set g
6	5	cv 1297	. . . . 5 class g
7	4, 3, 6	wf 3994	. . . 4 wff g:(t X. t)-->t
8	7, 2	wex 1326	. . 3 wff E.t g:(t X. t)-->t
9	8, 5	cab 1871	. 2 class {g | E.t g:(t X. t)-->t}
10	1, 9	wceq 1298	1 wff Magma = {g | E.t g:(t X. t)-->t}

This definition is referenced by:  ismgm 10367

Copyright terms: Public domain