This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = { 𝑔 ∣ ∃ 𝑡 𝑔 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmagm	⊢ Magma
1		vg	⊢ 𝑔
2		vt	⊢ 𝑡
3	1	cv	⊢ 𝑔
4	2	cv	⊢ 𝑡
5	4 4	cxp	⊢ ( 𝑡 × 𝑡 )
6	5 4 3	wf	⊢ 𝑔 : ( 𝑡 × 𝑡 ) ⟶ 𝑡
7	6 2	wex	⊢ ∃ 𝑡 𝑔 : ( 𝑡 × 𝑡 ) ⟶ 𝑡
8	7 1	cab	⊢ { 𝑔 ∣ ∃ 𝑡 𝑔 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 }
9	0 8	wceq	⊢ Magma = { 𝑔 ∣ ∃ 𝑡 𝑔 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 }