Definition df-bj-unc

Description: Define uncurrying. See also df-unc . (Contributed by BJ, 11-Apr-2020)

	Ref	Expression
Assertion	df-bj-unc	|- uncurry_ = ( x e. _V , y e. _V , z e. _V |-> ( f e. ( x -Set-> ( y -Set-> z ) ) |-> ( a e. x , b e. y |-> ( ( f ` a ) ` b ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cunc-	|- uncurry_
1		vx	|- x
2		cvv	|- _V
3		vy	|- y
4		vz	|- z
5		vf	|- f
6	1	cv	|- x
7		csethom	|- -Set->
8	3	cv	|- y
9	4	cv	|- z
10	8 9 7	co	|- ( y -Set-> z )
11	6 10 7	co	|- ( x -Set-> ( y -Set-> z ) )
12		va	|- a
13		vb	|- b
14	5	cv	|- f
15	12	cv	|- a
16	15 14	cfv	|- ( f ` a )
17	13	cv	|- b
18	17 16	cfv	|- ( ( f ` a ) ` b )
19	12 13 6 8 18	cmpo	|- ( a e. x , b e. y |-> ( ( f ` a ) ` b ) )
20	5 11 19	cmpt	|- ( f e. ( x -Set-> ( y -Set-> z ) ) |-> ( a e. x , b e. y |-> ( ( f ` a ) ` b ) ) )
21	1 3 4 2 2 2 20	cmpt3	|- ( x e. _V , y e. _V , z e. _V |-> ( f e. ( x -Set-> ( y -Set-> z ) ) |-> ( a e. x , b e. y |-> ( ( f ` a ) ` b ) ) ) )
22	0 21	wceq	|- uncurry_ = ( x e. _V , y e. _V , z e. _V |-> ( f e. ( x -Set-> ( y -Set-> z ) ) |-> ( a e. x , b e. y |-> ( ( f ` a ) ` b ) ) ) )