MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-unc Structured version   Visualization version   GIF version

Definition df-unc 7281
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
StepHypRef Expression
1 cF . . 3 class 𝐹
21cunc 7279 . 2 class uncurry 𝐹
3 vy . . . . 5 setvar 𝑦
43cv 1474 . . . 4 class 𝑦
5 vz . . . . 5 setvar 𝑧
65cv 1474 . . . 4 class 𝑧
7 vx . . . . . 6 setvar 𝑥
87cv 1474 . . . . 5 class 𝑥
98, 1cfv 5804 . . . 4 class (𝐹𝑥)
104, 6, 9wbr 4583 . . 3 wff 𝑦(𝐹𝑥)𝑧
1110, 7, 3, 5coprab 6550 . 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝑦(𝐹𝑥)𝑧}
122, 11wceq 1475 1 wff uncurry 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝑦(𝐹𝑥)𝑧}
Colors of variables: wff setvar class
This definition is referenced by:  unceq  32556  uncf  32558  uncov  32560  unccur  32562
  Copyright terms: Public domain W3C validator