Theorem relco 6073

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-opab 5148  df-xp 5637  df-rel 5638  df-co 5640

This theorem is referenced by:  cotrg  6074  dfco2  6209  resco  6214  coeq0  6220  coiun  6221  cocnvcnv2  6223  cores2  6224  co02  6225  co01  6226  coi1  6227  coass  6230  cossxp  6236  dfpo2  6260  fmptco  7082  cofunexg  7902  dftpos4  8195  ttrcltr  9637  ttrclco  9639  wunco  10656  relexprelg  15000  relexpaddg  15015  imasless  17504  znleval  21534  metustexhalf  24521  fcoinver  32674  fmptcof2  32730  cnvco1  35941  cnvco2  35942  opelco3  35957  txpss3v  36058  sscoid  36093  xrnss3v  38702  cononrel1  44021  cononrel2  44022  coiun1  44079  relexpaddss  44145  brco2f1o  44459  brco3f1o  44460  neicvgnvor  44543  sblpnf  44737  coxp  49308  xpco2  49332