Metamath Proof Explorer


Definition df-hom

Description: Define the hom-set component of a category. (Contributed by Mario Carneiro, 2-Jan-2017) Use its index-independent form homid instead. (New usage is discouraged.)

Ref Expression
Assertion df-hom Hom = Slot 14

Detailed syntax breakdown

Step Hyp Ref Expression
0 chom class Hom
1 c1 class 1
2 c4 class 4
3 1 2 cdc class 14
4 3 cslot class Slot 14
5 0 4 wceq wff Hom = Slot 14