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

Definition df-co 4380
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 4375 . 2 class (𝐴𝐵)
4 vx . . . . . . 7 setvar 𝑥
54cv 1284 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1284 . . . . . 6 class 𝑧
85, 7, 2wbr 3793 . . . . 5 wff 𝑥𝐵𝑧
9 vy . . . . . . 7 setvar 𝑦
109cv 1284 . . . . . 6 class 𝑦
117, 10, 1wbr 3793 . . . . 5 wff 𝑧𝐴𝑦
128, 11wa 102 . . . 4 wff (𝑥𝐵𝑧𝑧𝐴𝑦)
1312, 6wex 1422 . . 3 wff 𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)
1413, 4, 9copab 3846 . 2 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
153, 14wceq 1285 1 wff (𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
Colors of variables: wff set class
This definition is referenced by:  coss1  4519  coss2  4520  nfco  4529  brcog  4530  cnvco  4548  cotr  4736  relco  4849  coundi  4852  coundir  4853  cores  4854  xpcom  4894  dffun2  4942  funco  4970  xpcomco  6370
  Copyright terms: Public domain W3C validator