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

Definition df-cur1 25299
 Description: Definition of currying (1st 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-cur1
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-cur1
StepHypRef Expression
1 ccur1 25297 . 2
2 vf . . . . . . 7
32cv 1631 . . . . . 6
43wfun 5265 . . . . 5
53cdm 4705 . . . . . 6
65wrel 4710 . . . . 5
74, 6wa 358 . . . 4
8 vg . . . . . 6
98cv 1631 . . . . 5
10 vx . . . . . 6
115cdm 4705 . . . . . 6
12 c2nd 6137 . . . . . . . . 9
1310cv 1631 . . . . . . . . . . 11
1413csn 3653 . . . . . . . . . 10
15 cvv 2801 . . . . . . . . . 10
1614, 15cxp 4703 . . . . . . . . 9
1712, 16cres 4707 . . . . . . . 8
1817ccnv 4704 . . . . . . 7
193, 18ccom 4709 . . . . . 6
2010, 11, 19cmpt 4093 . . . . 5
219, 20wceq 1632 . . . 4
227, 21wa 358 . . 3
2322, 2, 8copab 4092 . 2
241, 23wceq 1632 1
 Colors of variables: wff set class This definition is referenced by:  cur1val  25301
 Copyright terms: Public domain W3C validator