Definition df-bj-unc 37118

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

Assertion

Ref	Expression
df-bj-unc	⊢ uncurry_ = (𝑥 ∈ V, 𝑦 ∈ V, 𝑧 ∈ V ↦ (𝑓 ∈ (𝑥 Set⟶ (𝑦 Set⟶ 𝑧)) ↦ (𝑎 ∈ 𝑥, 𝑏 ∈ 𝑦 ↦ ((𝑓‘𝑎)‘𝑏))))

Distinct variable group:   𝑥,𝑦,𝑧,𝑎,𝑏,𝑓

Detailed syntax breakdown of Definition df-bj-unc

Step	Hyp	Ref	Expression
1		cunc- 37117	. 2 class uncurry_
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		vz	. . 3 setvar 𝑧
5		cvv 3455	. . 3 class V
6		vf	. . . 4 setvar 𝑓
7	2	cv 1539	. . . . 5 class 𝑥
8	3	cv 1539	. . . . . 6 class 𝑦
9	4	cv 1539	. . . . . 6 class 𝑧
10		csethom 37107	. . . . . 6 class Set⟶
11	8, 9, 10	co 7394	. . . . 5 class (𝑦 Set⟶ 𝑧)
12	7, 11, 10	co 7394	. . . 4 class (𝑥 Set⟶ (𝑦 Set⟶ 𝑧))
13		va	. . . . 5 setvar 𝑎
14		vb	. . . . 5 setvar 𝑏
15	14	cv 1539	. . . . . 6 class 𝑏
16	13	cv 1539	. . . . . . 7 class 𝑎
17	6	cv 1539	. . . . . . 7 class 𝑓
18	16, 17	cfv 6519	. . . . . 6 class (𝑓‘𝑎)
19	15, 18	cfv 6519	. . . . 5 class ((𝑓‘𝑎)‘𝑏)
20	13, 14, 7, 8, 19	cmpo 7396	. . . 4 class (𝑎 ∈ 𝑥, 𝑏 ∈ 𝑦 ↦ ((𝑓‘𝑎)‘𝑏))
21	6, 12, 20	cmpt 5196	. . 3 class (𝑓 ∈ (𝑥 Set⟶ (𝑦 Set⟶ 𝑧)) ↦ (𝑎 ∈ 𝑥, 𝑏 ∈ 𝑦 ↦ ((𝑓‘𝑎)‘𝑏)))
22	2, 3, 4, 5, 5, 5, 21	cmpt3 37105	. 2 class (𝑥 ∈ V, 𝑦 ∈ V, 𝑧 ∈ V ↦ (𝑓 ∈ (𝑥 Set⟶ (𝑦 Set⟶ 𝑧)) ↦ (𝑎 ∈ 𝑥, 𝑏 ∈ 𝑦 ↦ ((𝑓‘𝑎)‘𝑏))))
23	1, 22	wceq 1540	1 wff uncurry_ = (𝑥 ∈ V, 𝑦 ∈ V, 𝑧 ∈ V ↦ (𝑓 ∈ (𝑥 Set⟶ (𝑦 Set⟶ 𝑧)) ↦ (𝑎 ∈ 𝑥, 𝑏 ∈ 𝑦 ↦ ((𝑓‘𝑎)‘𝑏))))

This definition is referenced by: (None)