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. catcone0
25. 0catg
26. 0cat
27. homffval
28. fnhomeqhomf
29. homfval
30. homffn
31. homfeq
32. homfeqd
33. homfeqbas
34. homfeqval
35. comfffval
36. comffval
37. comfval
38. comfffval2
39. comffval2
40. comfval2
41. comfffn
42. comffn
43. comfeq
44. comfeqd
45. comfeqval
46. catpropd
47. cidpropd