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

Definition df-cur 6290
Description: Define the currying of  F, which splits a function of two arguments into a function of the first argument, producing a function over the second argument. (Contributed by Mario Carneiro, 7-Jan-2017.)
Assertion
Ref Expression
df-cur  |- curry  F  =  ( x  e.  dom  dom 
F  |->  { <. y ,  z >.  |  <. x ,  y >. F z } )
Distinct variable group:    x, y, z, F

Detailed syntax breakdown of Definition df-cur
StepHypRef Expression
1 cF . . 3  class  F
21ccur 6288 . 2  class curry  F
3 vx . . 3  set  x
41cdm 4705 . . . 4  class  dom  F
54cdm 4705 . . 3  class  dom  dom  F
63cv 1631 . . . . . 6  class  x
7 vy . . . . . . 7  set  y
87cv 1631 . . . . . 6  class  y
96, 8cop 3656 . . . . 5  class  <. x ,  y >.
10 vz . . . . . 6  set  z
1110cv 1631 . . . . 5  class  z
129, 11, 1wbr 4039 . . . 4  wff  <. x ,  y >. F z
1312, 7, 10copab 4092 . . 3  class  { <. y ,  z >.  |  <. x ,  y >. F z }
143, 5, 13cmpt 4093 . 2  class  ( x  e.  dom  dom  F  |->  { <. y ,  z
>.  |  <. x ,  y >. F z } )
152, 14wceq 1632 1  wff curry  F  =  ( x  e.  dom  dom 
F  |->  { <. y ,  z >.  |  <. x ,  y >. F z } )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator