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

Definition df-uncf 15358
 Description: Define the uncurry functor, which can be defined equationally using evalF. Strictly speaking, the third category argument is not needed, since the resulting functor is extensionally equal regardless, but it is used in the equational definition and is too much work to remove. (Contributed by Mario Carneiro, 13-Jan-2017.)
Assertion
Ref Expression
df-uncf uncurryF evalF func func F ⟨,⟩F F
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-uncf
StepHypRef Expression
1 cuncf 15354 . 2 uncurryF
2 vc . . 3
3 vf . . 3
4 cvv 3095 . . 3
5 c1 9496 . . . . . 6
62cv 1382 . . . . . 6
75, 6cfv 5578 . . . . 5
8 c2 10591 . . . . . 6
98, 6cfv 5578 . . . . 5
10 cevlf 15352 . . . . 5 evalF
117, 9, 10co 6281 . . . 4 evalF
123cv 1382 . . . . . 6
13 cc0 9495 . . . . . . . 8
1413, 6cfv 5578 . . . . . . 7
15 c1stf 15312 . . . . . . 7 F
1614, 7, 15co 6281 . . . . . 6 F
17 ccofu 15099 . . . . . 6 func
1812, 16, 17co 6281 . . . . 5 func F
19 c2ndf 15313 . . . . . 6 F
2014, 7, 19co 6281 . . . . 5 F
21 cprf 15314 . . . . 5 ⟨,⟩F
2218, 20, 21co 6281 . . . 4 func F ⟨,⟩F F
2311, 22, 17co 6281 . . 3 evalF func func F ⟨,⟩F F
242, 3, 4, 4, 23cmpt2 6283 . 2 evalF func func F ⟨,⟩F F
251, 24wceq 1383 1 uncurryF evalF func func F ⟨,⟩F F
 Colors of variables: wff setvar class This definition is referenced by:  uncfval  15377
 Copyright terms: Public domain W3C validator