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	$$⊢uncurryF=\left\{⟨⟨x,y⟩,z⟩|yF\left(x\right)z\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	$$classF$$
1	0	cunc	$$classuncurryF$$
2		vx	$$setvarx$$
3		vy	$$setvary$$
4		vz	$$setvarz$$
5	3	cv	$$setvary$$
6	2	cv	$$setvarx$$
7	6 0	cfv	$$classF\left(x\right)$$
8	4	cv	$$setvarz$$
9	5 8 7	wbr	$$wffyF\left(x\right)z$$
10	9 2 3 4	coprab	$$class\left\{⟨⟨x,y⟩,z⟩|yF\left(x\right)z\right\}$$
11	1 10	wceq	$$wffuncurryF=\left\{⟨⟨x,y⟩,z⟩|yF\left(x\right)z\right\}$$