Definition df-cur 7280

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 7278	. 2 class curry 𝐹
3		vx	. . 3 setvar 𝑥
4	1	cdm 5038	. . . 4 class dom 𝐹
5	4	cdm 5038	. . 3 class dom dom 𝐹
6	3	cv 1474	. . . . . 6 class 𝑥
7		vy	. . . . . . 7 setvar 𝑦
8	7	cv 1474	. . . . . 6 class 𝑦
9	6, 8	cop 4131	. . . . 5 class ⟨𝑥, 𝑦⟩
10		vz	. . . . . 6 setvar 𝑧
11	10	cv 1474	. . . . 5 class 𝑧
12	9, 11, 1	wbr 4583	. . . 4 wff ⟨𝑥, 𝑦⟩𝐹𝑧
13	12, 7, 10	copab 4642	. . 3 class {⟨𝑦, 𝑧⟩ ∣ ⟨𝑥, 𝑦⟩𝐹𝑧}
14	3, 5, 13	cmpt 4643	. 2 class (𝑥 ∈ dom dom 𝐹 ↦ {⟨𝑦, 𝑧⟩ ∣ ⟨𝑥, 𝑦⟩𝐹𝑧})
15	2, 14	wceq 1475	1 wff curry 𝐹 = (𝑥 ∈ dom dom 𝐹 ↦ {⟨𝑦, 𝑧⟩ ∣ ⟨𝑥, 𝑦⟩𝐹𝑧})

This definition is referenced by:  mpt2curryd  7282  cureq  32555  curf  32557  curunc  32561  matunitlindf  32577