Mathbox for BJ < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bj-cur Structured version   Visualization version   GIF version

Definition df-bj-cur 32260
Assertion
Ref Expression
df-bj-cur curry_ = (𝑥 ∈ V, 𝑦 ∈ V, 𝑧 ∈ V ↦ (𝑓 ∈ ((𝑥 × 𝑦) Set𝑧) ↦ (𝑎𝑥 ↦ (𝑏𝑦 ↦ (𝑓‘⟨𝑎, 𝑏⟩)))))
Distinct variable group:   𝑥,𝑦,𝑧,𝑎,𝑏,𝑓

Detailed syntax breakdown of Definition df-bj-cur
StepHypRef Expression
1 ccur- 32258 . 2 class curry_
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 vz . . 3 setvar 𝑧
5 cvv 3173 . . 3 class V
6 vf . . . 4 setvar 𝑓
72cv 1474 . . . . . 6 class 𝑥
83cv 1474 . . . . . 6 class 𝑦
97, 8cxp 5036 . . . . 5 class (𝑥 × 𝑦)
104cv 1474 . . . . 5 class 𝑧
11 cfset 32256 . . . . 5 class Set
129, 10, 11co 6549 . . . 4 class ((𝑥 × 𝑦) Set𝑧)
13 va . . . . 5 setvar 𝑎
14 vb . . . . . 6 setvar 𝑏
1513cv 1474 . . . . . . . 8 class 𝑎
1614cv 1474 . . . . . . . 8 class 𝑏
1715, 16cop 4131 . . . . . . 7 class 𝑎, 𝑏
186cv 1474 . . . . . . 7 class 𝑓
1917, 18cfv 5804 . . . . . 6 class (𝑓‘⟨𝑎, 𝑏⟩)
2014, 8, 19cmpt 4643 . . . . 5 class (𝑏𝑦 ↦ (𝑓‘⟨𝑎, 𝑏⟩))
2113, 7, 20cmpt 4643 . . . 4 class (𝑎𝑥 ↦ (𝑏𝑦 ↦ (𝑓‘⟨𝑎, 𝑏⟩)))
226, 12, 21cmpt 4643 . . 3 class (𝑓 ∈ ((𝑥 × 𝑦) Set𝑧) ↦ (𝑎𝑥 ↦ (𝑏𝑦 ↦ (𝑓‘⟨𝑎, 𝑏⟩))))
232, 3, 4, 5, 5, 5, 22cmpt3 32254 . 2 class (𝑥 ∈ V, 𝑦 ∈ V, 𝑧 ∈ V ↦ (𝑓 ∈ ((𝑥 × 𝑦) Set𝑧) ↦ (𝑎𝑥 ↦ (𝑏𝑦 ↦ (𝑓‘⟨𝑎, 𝑏⟩)))))
241, 23wceq 1475 1 wff curry_ = (𝑥 ∈ V, 𝑦 ∈ V, 𝑧 ∈ V ↦ (𝑓 ∈ ((𝑥 × 𝑦) Set𝑧) ↦ (𝑎𝑥 ↦ (𝑏𝑦 ↦ (𝑓‘⟨𝑎, 𝑏⟩)))))
 Colors of variables: wff setvar class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator