Definition df-cur 7393

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.)

Assertion

Ref	Expression
df-cur	|- curry F = ( x e. dom dom F |-> { <. y , z >. | <. x , y >. F z } )

Distinct variable group:   x, y, z, F

Detailed syntax breakdown of Definition df-cur

Step	Hyp	Ref	Expression
1		cF	. . 3 class F
2	1	ccur 7391	. 2 class curry F
3		vx	. . 3 setvar x
4	1	cdm 5114	. . . 4 class dom F
5	4	cdm 5114	. . 3 class dom dom F
6	3	cv 1482	. . . . . 6 class x
7		vy	. . . . . . 7 setvar y
8	7	cv 1482	. . . . . 6 class y
9	6, 8	cop 4183	. . . . 5 class <. x , y >.
10		vz	. . . . . 6 setvar z
11	10	cv 1482	. . . . 5 class z
12	9, 11, 1	wbr 4653	. . . 4 wff <. x , y >. F z
13	12, 7, 10	copab 4712	. . 3 class { <. y , z >. | <. x , y >. F z }
14	3, 5, 13	cmpt 4729	. 2 class ( x e. dom dom F |-> { <. y , z >. | <. x , y >. F z } )
15	2, 14	wceq 1483	1 wff curry F = ( x e. dom dom F |-> { <. y , z >. | <. x , y >. F z } )

This definition is referenced by:  mpt2curryd  7395  cureq  33385  curf  33387  curunc  33391  matunitlindf  33407