Definition df-unc 8293

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 8291	. 2 class uncurry 𝐹
3		vy	. . . . 5 setvar 𝑦
4	3	cv 1539	. . . 4 class 𝑦
5		vz	. . . . 5 setvar 𝑧
6	5	cv 1539	. . . 4 class 𝑧
7		vx	. . . . . 6 setvar 𝑥
8	7	cv 1539	. . . . 5 class 𝑥
9	8, 1	cfv 6561	. . . 4 class (𝐹‘𝑥)
10	4, 6, 9	wbr 5143	. . 3 wff 𝑦(𝐹‘𝑥)𝑧
11	10, 7, 3, 5	coprab 7432	. 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝑦(𝐹‘𝑥)𝑧}
12	2, 11	wceq 1540	1 wff uncurry 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝑦(𝐹‘𝑥)𝑧}

This definition is referenced by:  unceq  37604  uncf  37606  uncov  37608  unccur  37610