df-bj-unc

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

		Ref	Expression
	Assertion	df-bj-unc	$⊢ uncurry_= (x \in V, y \in V, z \in V ⟼ (f \in (x \underset{Set}{⟶} (y \underset{Set}{⟶} z)) ⟼ (a \in x, b \in y ⟼ f (a) (b))))$

Step	Hyp	Ref	Expression
0		cunc-	$class uncurry_$
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		csethom	$class \underset{Set}{⟶}$
8	3	cv	$setvar y$
9	4	cv	$setvar z$
10	8 9 7	co	$class (y \underset{Set}{⟶} z)$
11	6 10 7	co	$class (x \underset{Set}{⟶} (y \underset{Set}{⟶} z))$
12		va	$setvar a$
13		vb	$setvar b$
14	5	cv	$setvar f$
15	12	cv	$setvar a$
16	15 14	cfv	$class f (a)$
17	13	cv	$setvar b$
18	17 16	cfv	$class f (a) (b)$
19	12 13 6 8 18	cmpo	$class (a \in x, b \in y ⟼ f (a) (b))$
20	5 11 19	cmpt	$class (f \in (x \underset{Set}{⟶} (y \underset{Set}{⟶} z)) ⟼ (a \in x, b \in y ⟼ f (a) (b)))$
21	1 3 4 2 2 2 20	cmpt3	$class (x \in V, y \in V, z \in V ⟼ (f \in (x \underset{Set}{⟶} (y \underset{Set}{⟶} z)) ⟼ (a \in x, b \in y ⟼ f (a) (b))))$
22	0 21	wceq	$wff uncurry_= (x \in V, y \in V, z \in V ⟼ (f \in (x \underset{Set}{⟶} (y \underset{Set}{⟶} z)) ⟼ (a \in x, b \in y ⟼ f (a) (b))))$

Metamath Proof Explorer