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

Definition df-co 4277
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 , and calls the operation "relative product." (Contributed by NM, 4-Jul-1994.)
Assertion
Ref Expression
df-co (AB) = {⟨x, y⟩ ∣ z(xBz zAy)}
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 4272 . 2 class (AB)
4 vx . . . . . . 7 setvar x
54cv 1225 . . . . . 6 class x
6 vz . . . . . . 7 setvar z
76cv 1225 . . . . . 6 class z
85, 7, 2wbr 3734 . . . . 5 wff xBz
9 vy . . . . . . 7 setvar y
109cv 1225 . . . . . 6 class y
117, 10, 1wbr 3734 . . . . 5 wff zAy
128, 11wa 97 . . . 4 wff (xBz zAy)
1312, 6wex 1358 . . 3 wff z(xBz zAy)
1413, 4, 9copab 3787 . 2 class {⟨x, y⟩ ∣ z(xBz zAy)}
153, 14wceq 1226 1 wff (AB) = {⟨x, y⟩ ∣ z(xBz zAy)}
Colors of variables: wff set class
This definition is referenced by:  coss1  4414  coss2  4415  nfco  4424  brcog  4425  cnvco  4443  cotr  4629  relco  4742  coundi  4745  coundir  4746  cores  4747  xpcom  4787  dffun2  4835  funco  4862
  Copyright terms: Public domain W3C validator