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

Theorem relco 6090
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 5557 . 2 (𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
21relopabi 5687 1 Rel (𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 396  wex 1771   class class class wbr 5057  ccom 5552  Rel wrel 5553
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-opab 5120  df-xp 5554  df-rel 5555  df-co 5557
This theorem is referenced by:  dfco2  6091  resco  6096  coeq0  6101  coiun  6102  cocnvcnv2  6104  cores2  6105  co02  6106  co01  6107  coi1  6108  coass  6111  cossxp  6116  fmptco  6883  cofunexg  7639  dftpos4  7900  wunco  10143  relexprelg  14385  relexpaddg  14400  imasless  16801  znleval  20629  metustexhalf  23093  fcoinver  30285  fmptcof2  30330  dfpo2  32888  cnvco1  32892  cnvco2  32893  opelco3  32915  txpss3v  33236  sscoid  33271  xrnss3v  35504  cononrel1  39832  cononrel2  39833  coiun1  39875  relexpaddss  39941  brco2f1o  40260  brco3f1o  40261  neicvgnvor  40344  sblpnf  40519
  Copyright terms: Public domain W3C validator