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

Definition df-co 4853
Description: Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. For example, (ex-co 22255) because (see cos0 13220) and (see df-e 13140). Note that Definition 7 of [Suppes] p. 63 reverses and , uses /. instead of o., and calls the operation "relative product." (Contributed by NM, 4-Jul-1994.)
Assertion
Ref Expression
df-co
Distinct variable groups:   , , ,   , , ,

Detailed syntax breakdown of Definition df-co
StepHypRef Expression
1 cA . . 3
2 cB . . 3
31, 2ccom 4848 . 2
4 vx . . . . . . 7
54cv 1661 . . . . . 6
6 vz . . . . . . 7
76cv 1661 . . . . . 6
85, 7, 2wbr 4302 . . . . 5
9 vy . . . . . . 7
109cv 1661 . . . . . 6
117, 10, 1wbr 4302 . . . . 5
128, 11wa 360 . . . 4
1312, 6wex 1557 . . 3
1413, 4, 9copab 4359 . 2
153, 14wceq 1662 1
Colors of variables: wff set class
This definition is referenced by:  coss1  4999  coss2  5000  nfco  5009  brcog  5010  cnvco  5029  cotr  5212  relco  5335  coundi  5338  coundir  5339  cores  5340  xpco  5376  dffun2  5427  funco  5455  xpcomco  7310  rtrclreclem.trans  25979
  Copyright terms: Public domain W3C validator