MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  relco Structured version   Visualization version   GIF version

Theorem relco 6108
Description: A composition is a relation. Exercise 24 of [TakeutiZaring] p. 25. (Contributed by NM, 26-Jan-1997.)
Assertion
Ref Expression
relco Rel (𝐴𝐵)

Proof of Theorem relco
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-co 5686 . 2 (𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
21relopabiv 5821 1 Rel (𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 397  wex 1782   class class class wbr 5149  ccom 5681  Rel wrel 5682
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-opab 5212  df-xp 5683  df-rel 5684  df-co 5686
This theorem is referenced by:  cotrg  6109  cotrgOLD  6110  cotrgOLDOLD  6111  dfco2  6245  resco  6250  coeq0  6255  coiun  6256  cocnvcnv2  6258  cores2  6259  co02  6260  co01  6261  coi1  6262  coass  6265  cossxp  6272  dfpo2  6296  fmptco  7127  cofunexg  7935  dftpos4  8230  ttrcltr  9711  ttrclco  9713  wunco  10728  relexprelg  14985  relexpaddg  15000  imasless  17486  znleval  21110  metustexhalf  24065  fcoinver  31835  fmptcof2  31882  cnvco1  34729  cnvco2  34730  opelco3  34746  txpss3v  34850  sscoid  34885  xrnss3v  37242  cononrel1  42345  cononrel2  42346  coiun1  42403  relexpaddss  42469  brco2f1o  42783  brco3f1o  42784  neicvgnvor  42867  sblpnf  43069
  Copyright terms: Public domain W3C validator