Definition df-bj-cur 33082

Description: Define currying. See also df-cur 7393. (Contributed by BJ, 11-Apr-2020.)

Assertion

Ref	Expression
df-bj-cur	|- curry_ = ( x e. _V , y e. _V , z e. _V |-> ( f e. ( ( x X. 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-cur

Step	Hyp	Ref	Expression
1		ccur- 33081	. 2 class curry_
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	. . . . . 6 class x
8	3	cv 1482	. . . . . 6 class y
9	7, 8	cxp 5112	. . . . 5 class ( x X. y )
10	4	cv 1482	. . . . 5 class z
11		csethom 33075	. . . . 5 class -Set->
12	9, 10, 11	co 6650	. . . 4 class ( ( x X. y ) -Set-> z )
13		va	. . . . 5 setvar a
14		vb	. . . . . 6 setvar b
15	13	cv 1482	. . . . . . . 8 class a
16	14	cv 1482	. . . . . . . 8 class b
17	15, 16	cop 4183	. . . . . . 7 class <. a , b >.
18	6	cv 1482	. . . . . . 7 class f
19	17, 18	cfv 5888	. . . . . 6 class ( f ` <. a , b >. )
20	14, 8, 19	cmpt 4729	. . . . 5 class ( b e. y |-> ( f ` <. a , b >. ) )
21	13, 7, 20	cmpt 4729	. . . 4 class ( a e. x |-> ( b e. y |-> ( f ` <. a , b >. ) ) )
22	6, 12, 21	cmpt 4729	. . 3 class ( f e. ( ( x X. y ) -Set-> z ) |-> ( a e. x |-> ( b e. y |-> ( f ` <. a , b >. ) ) ) )
23	2, 3, 4, 5, 5, 5, 22	cmpt3 33073	. 2 class ( x e. _V , y e. _V , z e. _V |-> ( f e. ( ( x X. y ) -Set-> z ) |-> ( a e. x |-> ( b e. y |-> ( f ` <. a , b >. ) ) ) ) )
24	1, 23	wceq 1483	1 wff curry_ = ( x e. _V , y e. _V , z e. _V |-> ( f e. ( ( x X. y ) -Set-> z ) |-> ( a e. x |-> ( b e. y |-> ( f ` <. a , b >. ) ) ) ) )

This definition is referenced by: (None)