Theorem relco 6082

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.

Step	Hyp	Ref	Expression
1		df-co 5650	. 2 ⊢ (𝐴 ∘ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)}
2	1	relopabiv 5786	1 ⊢ Rel (𝐴 ∘ 𝐵)

Syntax hints:   ∧ wa 395  ∃wex 1779   class class class wbr 5110   ∘ ccom 5645  Rel wrel 5646

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-opab 5173  df-xp 5647  df-rel 5648  df-co 5650

This theorem is referenced by:  cotrg  6083  cotrgOLD  6084  cotrgOLDOLD  6085  dfco2  6221  resco  6226  coeq0  6231  coiun  6232  cocnvcnv2  6234  cores2  6235  co02  6236  co01  6237  coi1  6238  coass  6241  cossxp  6248  dfpo2  6272  fmptco  7104  cofunexg  7930  dftpos4  8227  ttrcltr  9676  ttrclco  9678  wunco  10693  relexprelg  15011  relexpaddg  15026  imasless  17510  znleval  21471  metustexhalf  24451  fcoinver  32540  fmptcof2  32588  cnvco1  35753  cnvco2  35754  opelco3  35769  txpss3v  35873  sscoid  35908  xrnss3v  38361  cononrel1  43590  cononrel2  43591  coiun1  43648  relexpaddss  43714  brco2f1o  44028  brco3f1o  44029  neicvgnvor  44112  sblpnf  44306  coxp  48825  xpco2  48849