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

Detailed syntax breakdown

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