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

Definition df-hom 13232
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 13219 . 2  class  Hom
2 c1 8738 . . . 4  class  1
3 c4 9797 . . . 4  class  4
42, 3cdc 10124 . . 3  class ; 1 4
54cslot 13147 . 2  class Slot ; 1 4
61, 5wceq 1623 1  wff  Hom  = Slot ; 1 4
Colors of variables: wff set class
This definition is referenced by:  homndx  13319  homid  13320  resshom  13323  prdsvalstr  13353  prdsval  13355  oppchomfval  13617  oppcbas  13621  rescbas  13706  reschom  13707  rescco  13709  rescabs  13710  wunfunc  13773  wunnat  13830  catstr  13831  fuchom  13835  setchomfval  13911  catchomfval  13930  catcoppccl  13940  catcfuccl  13941  catcxpccl  13981
  Copyright terms: Public domain W3C validator