Definition df-unc

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	|- F
1	0	cunc	|- uncurry F
2		vx	|- x
3		vy	|- y
4		vz	|- z
5	3	cv	|- y
6	2	cv	|- x
7	6 0	cfv	|- ( F ` x )
8	4	cv	|- z
9	5 8 7	wbr	|- y ( F ` x ) z
10	9 2 3 4	coprab	|- { <. <. x , y >. , z >. | y ( F ` x ) z }
11	1 10	wceq	|- uncurry F = { <. <. x , y >. , z >. | y ( F ` x ) z }