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

Theorem relco 5436
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 )

Proof of Theorem relco
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-co 4949 . 2  |-  ( A  o.  B )  =  { <. x ,  y
>.  |  E. z
( x B z  /\  z A y ) }
21relopabi 5065 1  |-  Rel  ( A  o.  B )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369   E.wex 1587   class class class wbr 4392    o. ccom 4944   Rel wrel 4945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4513  ax-nul 4521  ax-pr 4631
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3072  df-dif 3431  df-un 3433  df-in 3435  df-ss 3442  df-nul 3738  df-if 3892  df-sn 3978  df-pr 3980  df-op 3984  df-opab 4451  df-xp 4946  df-rel 4947  df-co 4949
This theorem is referenced by:  dfco2  5437  resco  5442  coiun  5447  cocnvcnv2  5449  cores2  5450  co02  5451  co01  5452  coi1  5453  coass  5456  cossxp  5460  fmptco  5977  cofunexg  6643  dftpos4  6866  wunco  9003  imasless  14582  znleval  18098  metustexhalfOLD  20256  metustexhalf  20257  fmptcof2  26115  dfpo2  27701  cnvco1  27706  cnvco2  27707  opelco3  27725  txpss3v  28045  sscoid  28080  coeq0  29230  sblpnf  29736
  Copyright terms: Public domain W3C validator