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	$$⊢\mathrm{Magma}=\left\{g|\exists tg:t\times t⟶t\right\}$$

Detailed syntax breakdown

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