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

Definition df-co 4632
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 4627 . 2  class  ( A  o.  B )
4 vx . . . . . . 7  setvar  x
54cv 1352 . . . . . 6  class  x
6 vz . . . . . . 7  setvar  z
76cv 1352 . . . . . 6  class  z
85, 7, 2wbr 4000 . . . . 5  wff  x B z
9 vy . . . . . . 7  setvar  y
109cv 1352 . . . . . 6  class  y
117, 10, 1wbr 4000 . . . . 5  wff  z A y
128, 11wa 104 . . . 4  wff  ( x B z  /\  z A y )
1312, 6wex 1492 . . 3  wff  E. z
( x B z  /\  z A y )
1413, 4, 9copab 4060 . 2  class  { <. x ,  y >.  |  E. z ( x B z  /\  z A y ) }
153, 14wceq 1353 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  4778  coss2  4779  nfco  4788  elco  4789  brcog  4790  cnvco  4808  cotr  5006  relco  5123  coundi  5126  coundir  5127  cores  5128  xpcom  5171  dffun2  5222  funco  5252  xpcomco  6820
  Copyright terms: Public domain W3C validator