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

Theorem relco 5170
Description: A composition is a relation. Exercise 24 of [TakeutiZaring] p. 25. (Contributed by NM, 26-Jan-1997.)
Assertion
Ref Expression
relco  |-  Rel  ( A  o.  B )
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.

Proof of Theorem relco
StepHypRef Expression
1 df-co 4698 . 2  |-  ( A  o.  B )  =  { <. x ,  y
>.  |  E. z
( x B z  /\  z A y ) }
21relopabi 4811 1  |-  Rel  ( A  o.  B )
Colors of variables: wff set class
Syntax hints:    /\ wa 360   E.wex 1529   class class class wbr 4025    o. ccom 4693   Rel wrel 4694
This theorem is referenced by:  dfco2  5171  resco  5176  coiun  5181  cocnvcnv2  5183  cores2  5184  co02  5185  co01  5186  coi1  5187  coass  5190  cossxp  5194  coexg  5214  fmptco  5653  cofunexg  5701  dftpos4  6215  wunco  8351  imasless  13437  znleval  16503  dfpo2  23516  cnvco1  23521  cnvco2  23522  txpss3v  23827  coeq0  26231  sblpnf  26939
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pr 4214
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-opab 4080  df-xp 4695  df-rel 4696  df-co 4698
  Copyright terms: Public domain W3C validator