Definition df-cur 8054

Description: Define the currying of 𝐹, which splits a function of two arguments into a function of the first argument, producing a function over the second argument. (Contributed by Mario Carneiro, 7-Jan-2017.)

Assertion

Ref	Expression
df-cur	⊢ curry 𝐹 = (𝑥 ∈ dom dom 𝐹 ↦ {⟨𝑦, 𝑧⟩ ∣ ⟨𝑥, 𝑦⟩𝐹𝑧})

Distinct variable group:   𝑥,𝑦,𝑧,𝐹

Detailed syntax breakdown of Definition df-cur

Step	Hyp	Ref	Expression
1		cF	. . 3 class 𝐹
2	1	ccur 8052	. 2 class curry 𝐹
3		vx	. . 3 setvar 𝑥
4	1	cdm 5580	. . . 4 class dom 𝐹
5	4	cdm 5580	. . 3 class dom dom 𝐹
6	3	cv 1538	. . . . . 6 class 𝑥
7		vy	. . . . . . 7 setvar 𝑦
8	7	cv 1538	. . . . . 6 class 𝑦
9	6, 8	cop 4564	. . . . 5 class ⟨𝑥, 𝑦⟩
10		vz	. . . . . 6 setvar 𝑧
11	10	cv 1538	. . . . 5 class 𝑧
12	9, 11, 1	wbr 5070	. . . 4 wff ⟨𝑥, 𝑦⟩𝐹𝑧
13	12, 7, 10	copab 5132	. . 3 class {⟨𝑦, 𝑧⟩ ∣ ⟨𝑥, 𝑦⟩𝐹𝑧}
14	3, 5, 13	cmpt 5153	. 2 class (𝑥 ∈ dom dom 𝐹 ↦ {⟨𝑦, 𝑧⟩ ∣ ⟨𝑥, 𝑦⟩𝐹𝑧})
15	2, 14	wceq 1539	1 wff curry 𝐹 = (𝑥 ∈ dom dom 𝐹 ↦ {⟨𝑦, 𝑧⟩ ∣ ⟨𝑥, 𝑦⟩𝐹𝑧})

This definition is referenced by:  mpocurryd  8056  cureq  35680  curf  35682  curunc  35686  matunitlindf  35702