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 = ( x e. dom dom F |-> { <. y , z >. | <. x , y >. F z } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	|- F
1	0	ccur	|- curry F
2		vx	|- x
3	0	cdm	|- dom F
4	3	cdm	|- dom dom F
5		vy	|- y
6		vz	|- z
7	2	cv	|- x
8	5	cv	|- y
9	7 8	cop	|- <. x , y >.
10	6	cv	|- z
11	9 10 0	wbr	|- <. x , y >. F z
12	11 5 6	copab	|- { <. y , z >. | <. x , y >. F z }
13	2 4 12	cmpt	|- ( x e. dom dom F |-> { <. y , z >. | <. x , y >. F z } )
14	1 13	wceq	|- curry F = ( x e. dom dom F |-> { <. y , z >. | <. x , y >. F z } )