Definition df-cur 8292

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 8290	. 2 class curry 𝐹
3		vx	. . 3 setvar 𝑥
4	1	cdm 5685	. . . 4 class dom 𝐹
5	4	cdm 5685	. . 3 class dom dom 𝐹
6	3	cv 1539	. . . . . 6 class 𝑥
7		vy	. . . . . . 7 setvar 𝑦
8	7	cv 1539	. . . . . 6 class 𝑦
9	6, 8	cop 4632	. . . . 5 class ⟨𝑥, 𝑦⟩
10		vz	. . . . . 6 setvar 𝑧
11	10	cv 1539	. . . . 5 class 𝑧
12	9, 11, 1	wbr 5143	. . . 4 wff ⟨𝑥, 𝑦⟩𝐹𝑧
13	12, 7, 10	copab 5205	. . 3 class {⟨𝑦, 𝑧⟩ ∣ ⟨𝑥, 𝑦⟩𝐹𝑧}
14	3, 5, 13	cmpt 5225	. 2 class (𝑥 ∈ dom dom 𝐹 ↦ {⟨𝑦, 𝑧⟩ ∣ ⟨𝑥, 𝑦⟩𝐹𝑧})
15	2, 14	wceq 1540	1 wff curry 𝐹 = (𝑥 ∈ dom dom 𝐹 ↦ {⟨𝑦, 𝑧⟩ ∣ ⟨𝑥, 𝑦⟩𝐹𝑧})

This definition is referenced by:  mpocurryd  8294  cureq  37603  curf  37605  curunc  37609  matunitlindf  37625