# Metamath Proof Explorer

## 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{F}=\left({x}\in \mathrm{dom}\mathrm{dom}{F}⟼\left\{⟨{y},{z}⟩|⟨{x},{y}⟩{F}{z}\right\}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cF ${class}{F}$
1 0 ccur ${class}curry{F}$
2 vx ${setvar}{x}$
3 0 cdm ${class}\mathrm{dom}{F}$
4 3 cdm ${class}\mathrm{dom}\mathrm{dom}{F}$
5 vy ${setvar}{y}$
6 vz ${setvar}{z}$
7 2 cv ${setvar}{x}$
8 5 cv ${setvar}{y}$
9 7 8 cop ${class}⟨{x},{y}⟩$
10 6 cv ${setvar}{z}$
11 9 10 0 wbr ${wff}⟨{x},{y}⟩{F}{z}$
12 11 5 6 copab ${class}\left\{⟨{y},{z}⟩|⟨{x},{y}⟩{F}{z}\right\}$
13 2 4 12 cmpt ${class}\left({x}\in \mathrm{dom}\mathrm{dom}{F}⟼\left\{⟨{y},{z}⟩|⟨{x},{y}⟩{F}{z}\right\}\right)$
14 1 13 wceq ${wff}curry{F}=\left({x}\in \mathrm{dom}\mathrm{dom}{F}⟼\left\{⟨{y},{z}⟩|⟨{x},{y}⟩{F}{z}\right\}\right)$