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

Definition df-unc 7016
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
Distinct variable group:   , , ,

Detailed syntax breakdown of Definition df-unc
StepHypRef Expression
1 cF . . 3
21cunc 7014 . 2
3 vy . . . . 5
43cv 1394 . . . 4
5 vz . . . . 5
65cv 1394 . . . 4
7 vx . . . . . 6
87cv 1394 . . . . 5
98, 1cfv 5593 . . . 4
104, 6, 9wbr 4452 . . 3
1110, 7, 3, 5coprab 6297 . 2
122, 11wceq 1395 1
Colors of variables: wff setvar class
  Copyright terms: Public domain W3C validator