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

Definition df-co 4620
Description: Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. Note that Definition 7 of [Suppes] p. 63 reverses 𝐴 and 𝐵, uses a slash instead of , 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 class 𝐴
2 cB . . 3 class 𝐵
31, 2ccom 4615 . 2 class (𝐴𝐵)
4 vx . . . . . . 7 setvar 𝑥
54cv 1347 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1347 . . . . . 6 class 𝑧
85, 7, 2wbr 3989 . . . . 5 wff 𝑥𝐵𝑧
9 vy . . . . . . 7 setvar 𝑦
109cv 1347 . . . . . 6 class 𝑦
117, 10, 1wbr 3989 . . . . 5 wff 𝑧𝐴𝑦
128, 11wa 103 . . . 4 wff (𝑥𝐵𝑧𝑧𝐴𝑦)
1312, 6wex 1485 . . 3 wff 𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)
1413, 4, 9copab 4049 . 2 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
153, 14wceq 1348 1 wff (𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
Colors of variables: wff set class
This definition is referenced by:  coss1  4766  coss2  4767  nfco  4776  elco  4777  brcog  4778  cnvco  4796  cotr  4992  relco  5109  coundi  5112  coundir  5113  cores  5114  xpcom  5157  dffun2  5208  funco  5238  xpcomco  6804
  Copyright terms: Public domain W3C validator