This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-unc

Description: Define the uncurrying of F , which takes a function producing functions, and transforms it into a two-argument function. (Contributed by Mario Carneiro, 7-Jan-2017)

		Ref	Expression
	Assertion	df-unc	$⊢ uncurry F = \{⟨⟨x, y⟩, z⟩ \| y F (x) z\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	$class F$
1	0	cunc	$class uncurry F$
2		vx	$setvar x$
3		vy	$setvar y$
4		vz	$setvar z$
5	3	cv	$setvar y$
6	2	cv	$setvar x$
7	6 0	cfv	$class F (x)$
8	4	cv	$setvar z$
9	5 8 7	wbr	$wff y F (x) z$
10	9 2 3 4	coprab	$class \{⟨⟨x, y⟩, z⟩ \| y F (x) z\}$
11	1 10	wceq	$wff uncurry F = \{⟨⟨x, y⟩, z⟩ \| y F (x) z\}$