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

Definition df-idfu 15764
 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 15760 . 2 idfunc
2 vt . . 3
3 ccat 15570 . . 3
4 vb . . . 4
52cv 1436 . . . . 5
6 cbs 15121 . . . . 5
75, 6cfv 5601 . . . 4
8 cid 4763 . . . . . 6
94cv 1436 . . . . . 6
108, 9cres 4855 . . . . 5
11 vz . . . . . 6
129, 9cxp 4851 . . . . . 6
1311cv 1436 . . . . . . . 8
14 chom 15201 . . . . . . . . 9
155, 14cfv 5601 . . . . . . . 8
1613, 15cfv 5601 . . . . . . 7
178, 16cres 4855 . . . . . 6
1811, 12, 17cmpt 4482 . . . . 5
1910, 18cop 4004 . . . 4
204, 7, 19csb 3395 . . 3
212, 3, 20cmpt 4482 . 2
221, 21wceq 1437 1 idfunc
 Colors of variables: wff setvar class This definition is referenced by:  idfuval  15781
 Copyright terms: Public domain W3C validator