Mathbox for Frédéric Liné < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-cur2 Unicode version

Definition df-cur2 25300
 Description: Definition of currying (2nd sort). Currying the operation consists in creating a mapping that returns for every value of the partial application of to . (Contributed by FL, 24-Jan-2010.)
Assertion
Ref Expression
df-cur2
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-cur2
StepHypRef Expression
1 ccur2 25298 . 2
2 vf . . . . . 6
32cv 1631 . . . . 5
43wfun 5265 . . . 4
53cdm 4705 . . . . 5
65wrel 4710 . . . 4
7 vg . . . . . 6
87cv 1631 . . . . 5
9 vx . . . . . 6
105crn 4706 . . . . . 6
11 c1st 6136 . . . . . . . . 9
12 cvv 2801 . . . . . . . . . 10
139cv 1631 . . . . . . . . . . 11
1413csn 3653 . . . . . . . . . 10
1512, 14cxp 4703 . . . . . . . . 9
1611, 15cres 4707 . . . . . . . 8
1716ccnv 4704 . . . . . . 7
183, 17ccom 4709 . . . . . 6
199, 10, 18cmpt 4093 . . . . 5
208, 19wceq 1632 . . . 4
214, 6, 20w3a 934 . . 3
2221, 2, 7copab 4092 . 2
231, 22wceq 1632 1
 Colors of variables: wff set class
 Copyright terms: Public domain W3C validator