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

Definition df-unc 6275
Description: Define the uncurrying of  F, 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  F  =  { <. <. x ,  y
>. ,  z >.  |  y ( F `  x ) z }
Distinct variable group:    x, y, z, F

Detailed syntax breakdown of Definition df-unc
StepHypRef Expression
1 cF . . 3  class  F
21cunc 6273 . 2  class uncurry  F
3 vy . . . . 5  set  y
43cv 1622 . . . 4  class  y
5 vz . . . . 5  set  z
65cv 1622 . . . 4  class  z
7 vx . . . . . 6  set  x
87cv 1622 . . . . 5  class  x
98, 1cfv 5255 . . . 4  class  ( F `
 x )
104, 6, 9wbr 4023 . . 3  wff  y ( F `  x ) z
1110, 7, 3, 5coprab 5859 . 2  class  { <. <.
x ,  y >. ,  z >.  |  y ( F `  x
) z }
122, 11wceq 1623 1  wff uncurry  F  =  { <. <. x ,  y
>. ,  z >.  |  y ( F `  x ) z }
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator