Definition df-unc 7394

Description: Define the uncurrying of F, which takes a function producing functions, and transforms it into a two-argument function. (Contributed by Mario Carneiro, 7-Jan-2017.)

Assertion

Ref	Expression
df-unc	|- uncurry F = { <. <. x , y >. , z >. | y ( F ` x ) z }

Distinct variable group:   x, y, z, F

Detailed syntax breakdown of Definition df-unc

Step	Hyp	Ref	Expression
1		cF	. . 3 class F
2	1	cunc 7392	. 2 class uncurry F
3		vy	. . . . 5 setvar y
4	3	cv 1482	. . . 4 class y
5		vz	. . . . 5 setvar z
6	5	cv 1482	. . . 4 class z
7		vx	. . . . . 6 setvar x
8	7	cv 1482	. . . . 5 class x
9	8, 1	cfv 5888	. . . 4 class ( F ` x )
10	4, 6, 9	wbr 4653	. . 3 wff y ( F ` x ) z
11	10, 7, 3, 5	coprab 6651	. 2 class { <. <. x , y >. , z >. | y ( F ` x ) z }
12	2, 11	wceq 1483	1 wff uncurry F = { <. <. x , y >. , z >. | y ( F ` x ) z }

This definition is referenced by:  unceq  33386  uncf  33388  uncov  33390  unccur  33392