Metamath Proof Explorer

Table of Contents - 8.1.1. Categories

1. ccat
2. ccid
3. chomf
4. ccomf
5. df-cat
6. df-cid
7. df-homf
8. df-comf
9. iscat
10. iscatd
11. catidex
12. catideu
13. cidfval
14. cidval
15. cidffn
16. cidfn
17. catidd
18. iscatd2
19. catidcl
20. catlid
21. catrid
22. catcocl
23. catass
24. 0catg
25. 0cat
26. homffval
27. fnhomeqhomf
28. homfval
29. homffn
30. homfeq
31. homfeqd
32. homfeqbas
33. homfeqval
34. comfffval
35. comffval
36. comfval
37. comfffval2
38. comffval2
39. comfval2
40. comfffn
41. comffn
42. comfeq
43. comfeqd
44. comfeqval
45. catpropd
46. cidpropd