ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-co Unicode version

Definition df-co 4410
Description: Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. Note that Definition 7 of [Suppes] p. 63 reverses  A and  B, uses a slash instead of  o., and calls the operation "relative product." (Contributed by NM, 4-Jul-1994.)
Assertion
Ref Expression
df-co  |-  ( A  o.  B )  =  { <. x ,  y
>.  |  E. z
( x B z  /\  z A y ) }
Distinct variable groups:    x, y, z, A    x, B, y, z

Detailed syntax breakdown of Definition df-co
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
31, 2ccom 4405 . 2  class  ( A  o.  B )
4 vx . . . . . . 7  setvar  x
54cv 1284 . . . . . 6  class  x
6 vz . . . . . . 7  setvar  z
76cv 1284 . . . . . 6  class  z
85, 7, 2wbr 3811 . . . . 5  wff  x B z
9 vy . . . . . . 7  setvar  y
109cv 1284 . . . . . 6  class  y
117, 10, 1wbr 3811 . . . . 5  wff  z A y
128, 11wa 102 . . . 4  wff  ( x B z  /\  z A y )
1312, 6wex 1422 . . 3  wff  E. z
( x B z  /\  z A y )
1413, 4, 9copab 3864 . 2  class  { <. x ,  y >.  |  E. z ( x B z  /\  z A y ) }
153, 14wceq 1285 1  wff  ( A  o.  B )  =  { <. x ,  y
>.  |  E. z
( x B z  /\  z A y ) }
Colors of variables: wff set class
This definition is referenced by:  coss1  4549  coss2  4550  nfco  4559  elco  4560  brcog  4561  cnvco  4579  cotr  4768  relco  4883  coundi  4886  coundir  4887  cores  4888  xpcom  4931  dffun2  4979  funco  5007  xpcomco  6472
  Copyright terms: Public domain W3C validator