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

Theorem relco 6126
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 5694 . 2 (𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
21relopabiv 5830 1 Rel (𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 395  wex 1779   class class class wbr 5143  ccom 5689  Rel wrel 5690
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-opab 5206  df-xp 5691  df-rel 5692  df-co 5694
This theorem is referenced by:  cotrg  6127  cotrgOLD  6128  cotrgOLDOLD  6129  dfco2  6265  resco  6270  coeq0  6275  coiun  6276  cocnvcnv2  6278  cores2  6279  co02  6280  co01  6281  coi1  6282  coass  6285  cossxp  6292  dfpo2  6316  fmptco  7149  cofunexg  7973  dftpos4  8270  ttrcltr  9756  ttrclco  9758  wunco  10773  relexprelg  15077  relexpaddg  15092  imasless  17585  znleval  21573  metustexhalf  24569  fcoinver  32617  fmptcof2  32667  cnvco1  35759  cnvco2  35760  opelco3  35775  txpss3v  35879  sscoid  35914  xrnss3v  38373  cononrel1  43607  cononrel2  43608  coiun1  43665  relexpaddss  43731  brco2f1o  44045  brco3f1o  44046  neicvgnvor  44129  sblpnf  44329  coxp  48744
  Copyright terms: Public domain W3C validator