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

Definition df-uncf 15184
Description: Define the uncurry functor, which can be defined equationally using . 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
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-uncf
StepHypRef Expression
1 cuncf 15180 . 2
2 vc . . 3
3 vf . . 3
4 cvv 3081 . . 3
5 c1 9420 . . . . . 6
62cv 1369 . . . . . 6
75, 6cfv 5537 . . . . 5
8 c2 10509 . . . . . 6
98, 6cfv 5537 . . . . 5
10 cevlf 15178 . . . . 5
117, 9, 10co 6222 . . . 4
123cv 1369 . . . . . 6
13 cc0 9419 . . . . . . . 8
1413, 6cfv 5537 . . . . . . 7
15 c1stf 15138 . . . . . . 7
1614, 7, 15co 6222 . . . . . 6
17 ccofu 14925 . . . . . 6
1812, 16, 17co 6222 . . . . 5
19 c2ndf 15139 . . . . . 6
2014, 7, 19co 6222 . . . . 5
21 cprf 15140 . . . . 5
2218, 20, 21co 6222 . . . 4
2311, 22, 17co 6222 . . 3
242, 3, 4, 4, 23cmpt2 6224 . 2
251, 24wceq 1370 1
Colors of variables: wff setvar class
This definition is referenced by:  uncfval  15203
  Copyright terms: Public domain W3C validator