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

Definition df-co 4871
Description: Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. For example, (ex-co 22767) because (see cos0 13281) and (see df-e 13201). 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 4866 . 2
4 vx . . . . . . 7
54cv 1669 . . . . . 6
6 vz . . . . . . 7
76cv 1669 . . . . . 6
85, 7, 2wbr 4318 . . . . 5
9 vy . . . . . . 7
109cv 1669 . . . . . 6
117, 10, 1wbr 4318 . . . . 5
128, 11wa 360 . . . 4
1312, 6wex 1565 . . 3
1413, 4, 9copab 4375 . 2
153, 14wceq 1670 1
Colors of variables: wff set class
This definition is referenced by:  coss1  5017  coss2  5018  nfco  5027  brcog  5028  cnvco  5047  cotr  5233  relco  5356  coundi  5359  coundir  5360  cores  5361  xpco  5397  dffun2  5448  funco  5476  xpcomco  7363  rtrclreclem.trans  26488
  Copyright terms: Public domain W3C validator