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

Definition df-co 5013
Description: Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. For example, (ex-co 25159) because (see cos0 13885) and (see df-e 13804). 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 5008 . 2
4 vx . . . . . . 7
54cv 1394 . . . . . 6
6 vz . . . . . . 7
76cv 1394 . . . . . 6
85, 7, 2wbr 4452 . . . . 5
9 vy . . . . . . 7
109cv 1394 . . . . . 6
117, 10, 1wbr 4452 . . . . 5
128, 11wa 369 . . . 4
1312, 6wex 1612 . . 3
1413, 4, 9copab 4509 . 2
153, 14wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  coss1  5163  coss2  5164  nfco  5173  brcog  5174  cnvco  5193  cotrg  5383  relco  5510  coundi  5513  coundir  5514  cores  5515  xpco  5552  dffun2  5603  funco  5631  xpcomco  7627  rtrclreclem.trans  29069  coss12d  37759  xpcogend  37773  trclubg  37785
  Copyright terms: Public domain W3C validator