Definition df-mgmOLD 35986

Description: Obsolete version of df-mgm 18307 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 = {𝑔 ∣ ∃𝑡 𝑔:(𝑡 × 𝑡)⟶𝑡}

Distinct variable group:   𝑡,𝑔

Detailed syntax breakdown of Definition df-mgmOLD

Step	Hyp	Ref	Expression
1		cmagm 35985	. 2 class Magma
2		vt	. . . . . . 7 setvar 𝑡
3	2	cv 1540	. . . . . 6 class 𝑡
4	3, 3	cxp 5586	. . . . 5 class (𝑡 × 𝑡)
5		vg	. . . . . 6 setvar 𝑔
6	5	cv 1540	. . . . 5 class 𝑔
7	4, 3, 6	wf 6426	. . . 4 wff 𝑔:(𝑡 × 𝑡)⟶𝑡
8	7, 2	wex 1785	. . 3 wff ∃𝑡 𝑔:(𝑡 × 𝑡)⟶𝑡
9	8, 5	cab 2716	. 2 class {𝑔 ∣ ∃𝑡 𝑔:(𝑡 × 𝑡)⟶𝑡}
10	1, 9	wceq 1541	1 wff Magma = {𝑔 ∣ ∃𝑡 𝑔:(𝑡 × 𝑡)⟶𝑡}

This definition is referenced by:  ismgmOLD  35987