Definition df-unc 8010

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

Assertion

Ref	Expression
df-unc	⊢ uncurry 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝑦(𝐹‘𝑥)𝑧}

Distinct variable group:   𝑥,𝑦,𝑧,𝐹

Detailed syntax breakdown of Definition df-unc

Step	Hyp	Ref	Expression
1		cF	. . 3 class 𝐹
2	1	cunc 8008	. 2 class uncurry 𝐹
3		vy	. . . . 5 setvar 𝑦
4	3	cv 1542	. . . 4 class 𝑦
5		vz	. . . . 5 setvar 𝑧
6	5	cv 1542	. . . 4 class 𝑧
7		vx	. . . . . 6 setvar 𝑥
8	7	cv 1542	. . . . 5 class 𝑥
9	8, 1	cfv 6380	. . . 4 class (𝐹‘𝑥)
10	4, 6, 9	wbr 5053	. . 3 wff 𝑦(𝐹‘𝑥)𝑧
11	10, 7, 3, 5	coprab 7214	. 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝑦(𝐹‘𝑥)𝑧}
12	2, 11	wceq 1543	1 wff uncurry 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝑦(𝐹‘𝑥)𝑧}

This definition is referenced by:  unceq  35491  uncf  35493  uncov  35495  unccur  35497