Mathbox for Frédéric Liné < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-homOLD Unicode version

Definition df-homOLD 25889
 Description: is a function which returns for each pair of objects the morphisms whose domain is and codomain . JFM CAT1 def. 6 (Contributed by FL, 6-May-2007.)
Assertion
Ref Expression
df-homOLD
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-homOLD
StepHypRef Expression
1 chomOLD 25888 . 2
2 vx . . 3
3 ccatOLD 25855 . . 3
4 va . . . 4
5 vb . . . 4
62cv 1631 . . . . . 6
7 cid_ 25817 . . . . . 6
86, 7cfv 5271 . . . . 5
98cdm 4705 . . . 4
10 vf . . . . . . . . 9
1110cv 1631 . . . . . . . 8
12 cdom_ 25815 . . . . . . . . 9
136, 12cfv 5271 . . . . . . . 8
1411, 13cfv 5271 . . . . . . 7
154cv 1631 . . . . . . 7
1614, 15wceq 1632 . . . . . 6
17 ccod_ 25816 . . . . . . . . 9
186, 17cfv 5271 . . . . . . . 8
1911, 18cfv 5271 . . . . . . 7
205cv 1631 . . . . . . 7
2119, 20wceq 1632 . . . . . 6
2216, 21wa 358 . . . . 5
2313cdm 4705 . . . . 5
2422, 10, 23crab 2560 . . . 4
254, 5, 9, 9, 24cmpt2 5876 . . 3
262, 3, 25cmpt 4093 . 2
271, 26wceq 1632 1
 Colors of variables: wff set class This definition is referenced by:  ishoma  25890
 Copyright terms: Public domain W3C validator