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

Definition df-hom 13323
Description: Define the hom-set component of a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
Assertion
Ref Expression
df-hom  |-  Hom  = Slot ; 1 4

Detailed syntax breakdown of Definition df-hom
StepHypRef Expression
1 chom 13310 . 2  class  Hom
2 c1 8825 . . . 4  class  1
3 c4 9884 . . . 4  class  4
42, 3cdc 10213 . . 3  class ; 1 4
54cslot 13238 . 2  class Slot ; 1 4
61, 5wceq 1642 1  wff  Hom  = Slot ; 1 4
Colors of variables: wff set class
This definition is referenced by:  homndx  13412  homid  13413  resshom  13416  prdsvalstr  13446  prdsval  13448  oppchomfval  13710  oppcbas  13714  rescbas  13799  reschom  13800  rescco  13802  rescabs  13803  wunfunc  13866  wunnat  13923  catstr  13924  fuchom  13928  setchomfval  14004  catchomfval  14023  catcoppccl  14033  catcfuccl  14034  catcxpccl  14074
  Copyright terms: Public domain W3C validator