df-bj-cur

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

		Ref	Expression
	Assertion	df-bj-cur	$⊢ curry_= (x \in V, y \in V, z \in V ⟼ (f \in ((x \times y) \underset{Set}{⟶} z) ⟼ (a \in x ⟼ (b \in y ⟼ f (⟨a, b⟩)))))$

Step	Hyp	Ref	Expression
0		ccur-	$class curry_$
1		vx	$setvar x$
2		cvv	$class V$
3		vy	$setvar y$
4		vz	$setvar z$
5		vf	$setvar f$
6	1	cv	$setvar x$
7	3	cv	$setvar y$
8	6 7	cxp	$class (x \times y)$
9		csethom	$class \underset{Set}{⟶}$
10	4	cv	$setvar z$
11	8 10 9	co	$class ((x \times y) \underset{Set}{⟶} z)$
12		va	$setvar a$
13		vb	$setvar b$
14	5	cv	$setvar f$
15	12	cv	$setvar a$
16	13	cv	$setvar b$
17	15 16	cop	$class ⟨a, b⟩$
18	17 14	cfv	$class f (⟨a, b⟩)$
19	13 7 18	cmpt	$class (b \in y ⟼ f (⟨a, b⟩))$
20	12 6 19	cmpt	$class (a \in x ⟼ (b \in y ⟼ f (⟨a, b⟩)))$
21	5 11 20	cmpt	$class (f \in ((x \times y) \underset{Set}{⟶} z) ⟼ (a \in x ⟼ (b \in y ⟼ f (⟨a, b⟩))))$
22	1 3 4 2 2 2 21	cmpt3	$class (x \in V, y \in V, z \in V ⟼ (f \in ((x \times y) \underset{Set}{⟶} z) ⟼ (a \in x ⟼ (b \in y ⟼ f (⟨a, b⟩)))))$
23	0 22	wceq	$wff curry_= (x \in V, y \in V, z \in V ⟼ (f \in ((x \times y) \underset{Set}{⟶} z) ⟼ (a \in x ⟼ (b \in y ⟼ f (⟨a, b⟩)))))$

Metamath Proof Explorer