Definition df-cur

Description: Define the currying of F , 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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	⊢ 𝐹
1	0	ccur	⊢ curry 𝐹
2		vx	⊢ 𝑥
3	0	cdm	⊢ dom 𝐹
4	3	cdm	⊢ dom dom 𝐹
5		vy	⊢ 𝑦
6		vz	⊢ 𝑧
7	2	cv	⊢ 𝑥
8	5	cv	⊢ 𝑦
9	7 8	cop	⊢ ⟨ 𝑥 , 𝑦 ⟩
10	6	cv	⊢ 𝑧
11	9 10 0	wbr	⊢ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧
12	11 5 6	copab	⊢ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 }
13	2 4 12	cmpt	⊢ ( 𝑥 ∈ dom dom 𝐹 ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 } )
14	1 13	wceq	⊢ curry 𝐹 = ( 𝑥 ∈ dom dom 𝐹 ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 } )