Definition df-bj-unc 33084

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

Assertion

Ref	Expression
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 ) ) ) )

Distinct variable group:   x, y, z, a, b, f

Detailed syntax breakdown of Definition df-bj-unc

Step	Hyp	Ref	Expression
1		cunc- 33083	. 2 class uncurry_
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		vz	. . 3 setvar z
5		cvv 3200	. . 3 class _V
6		vf	. . . 4 setvar f
7	2	cv 1482	. . . . 5 class x
8	3	cv 1482	. . . . . 6 class y
9	4	cv 1482	. . . . . 6 class z
10		csethom 33075	. . . . . 6 class -Set->
11	8, 9, 10	co 6650	. . . . 5 class ( y -Set-> z )
12	7, 11, 10	co 6650	. . . 4 class ( x -Set-> ( y -Set-> z ) )
13		va	. . . . 5 setvar a
14		vb	. . . . 5 setvar b
15	14	cv 1482	. . . . . 6 class b
16	13	cv 1482	. . . . . . 7 class a
17	6	cv 1482	. . . . . . 7 class f
18	16, 17	cfv 5888	. . . . . 6 class ( f ` a )
19	15, 18	cfv 5888	. . . . 5 class ( ( f ` a ) ` b )
20	13, 14, 7, 8, 19	cmpt2 6652	. . . 4 class ( a e. x , b e. y |-> ( ( f ` a ) ` b ) )
21	6, 12, 20	cmpt 4729	. . 3 class ( f e. ( x -Set-> ( y -Set-> z ) ) |-> ( a e. x , b e. y |-> ( ( f ` a ) ` b ) ) )
22	2, 3, 4, 5, 5, 5, 21	cmpt3 33073	. 2 class ( 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 ) ) ) )
23	1, 22	wceq 1483	1 wff 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 ) ) ) )

This definition is referenced by: (None)