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

Definition df-idfu 14048
 Description: Define the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.)
Assertion
Ref Expression
df-idfu idfunc
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-idfu
StepHypRef Expression
1 cidfu 14044 . 2 idfunc
2 vt . . 3
3 ccat 13881 . . 3
4 vb . . . 4
52cv 1651 . . . . 5
6 cbs 13461 . . . . 5
75, 6cfv 5446 . . . 4
8 cid 4485 . . . . . 6
94cv 1651 . . . . . 6
108, 9cres 4872 . . . . 5
11 vz . . . . . 6
129, 9cxp 4868 . . . . . 6
1311cv 1651 . . . . . . . 8
14 chom 13532 . . . . . . . . 9
155, 14cfv 5446 . . . . . . . 8
1613, 15cfv 5446 . . . . . . 7
178, 16cres 4872 . . . . . 6
1811, 12, 17cmpt 4258 . . . . 5
1910, 18cop 3809 . . . 4
204, 7, 19csb 3243 . . 3
212, 3, 20cmpt 4258 . 2
221, 21wceq 1652 1 idfunc
 Colors of variables: wff set class This definition is referenced by:  idfuval  14065
 Copyright terms: Public domain W3C validator