Theorem relco 6075

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 5641	. 2 ⊢ (𝐴 ∘ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)}
2	1	relopabiv 5777	1 ⊢ Rel (𝐴 ∘ 𝐵)

Syntax hints:   ∧ wa 395  ∃wex 1781   class class class wbr 5100   ∘ ccom 5636  Rel wrel 5637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920  df-opab 5163  df-xp 5638  df-rel 5639  df-co 5641

This theorem is referenced by:  cotrg  6076  dfco2  6211  resco  6216  coeq0  6222  coiun  6223  cocnvcnv2  6225  cores2  6226  co02  6227  co01  6228  coi1  6229  coass  6232  cossxp  6238  dfpo2  6262  fmptco  7084  cofunexg  7903  dftpos4  8197  ttrcltr  9637  ttrclco  9639  wunco  10656  relexprelg  14973  relexpaddg  14988  imasless  17473  znleval  21521  metustexhalf  24512  fcoinver  32691  fmptcof2  32747  cnvco1  35975  cnvco2  35976  opelco3  35991  txpss3v  36092  sscoid  36127  xrnss3v  38632  cononrel1  43950  cononrel2  43951  coiun1  44008  relexpaddss  44074  brco2f1o  44388  brco3f1o  44389  neicvgnvor  44472  sblpnf  44666  coxp  49192  xpco2  49216