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

Definition df-co 4555
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 4550 . 2 class (𝐴𝐵)
4 vx . . . . . . 7 setvar 𝑥
54cv 1331 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1331 . . . . . 6 class 𝑧
85, 7, 2wbr 3936 . . . . 5 wff 𝑥𝐵𝑧
9 vy . . . . . . 7 setvar 𝑦
109cv 1331 . . . . . 6 class 𝑦
117, 10, 1wbr 3936 . . . . 5 wff 𝑧𝐴𝑦
128, 11wa 103 . . . 4 wff (𝑥𝐵𝑧𝑧𝐴𝑦)
1312, 6wex 1469 . . 3 wff 𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)
1413, 4, 9copab 3995 . 2 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
153, 14wceq 1332 1 wff (𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
Colors of variables: wff set class
This definition is referenced by:  coss1  4701  coss2  4702  nfco  4711  elco  4712  brcog  4713  cnvco  4731  cotr  4927  relco  5044  coundi  5047  coundir  5048  cores  5049  xpcom  5092  dffun2  5140  funco  5170  xpcomco  6727
  Copyright terms: Public domain W3C validator