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

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

Proof of Theorem relco
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-co 4841 . 2
21relopabi 4954 1
 Colors of variables: wff set class Syntax hints:   wa 359  wex 1547   class class class wbr 4167   ccom 4836   wrel 4837 This theorem is referenced by:  dfco2  5323  resco  5328  coiun  5333  cocnvcnv2  5335  cores2  5336  co02  5337  co01  5338  coi1  5339  coass  5342  cossxp  5346  fmptco  5854  cofunexg  5912  dftpos4  6448  wunco  8555  imasless  13706  znleval  16776  metustexhalfOLD  18532  metustexhalf  18533  fmptcof2  23996  dfpo2  25295  cnvco1  25300  cnvco2  25301  txpss3v  25601  dffun10  25636  coeq0  26662  sblpnf  27369 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2382  ax-sep 4285  ax-nul 4293  ax-pr 4358 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2526  df-ne 2566  df-ral 2668  df-rex 2669  df-rab 2672  df-v 2915  df-dif 3280  df-un 3282  df-in 3284  df-ss 3291  df-nul 3586  df-if 3697  df-sn 3777  df-pr 3778  df-op 3780  df-opab 4222  df-xp 4838  df-rel 4839  df-co 4841
 Copyright terms: Public domain W3C validator