Theorem relco 6079

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

Syntax hints:   ∧ wa 395  ∃wex 1779   class class class wbr 5107   ∘ ccom 5642  Rel wrel 5643

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-ss 3931  df-opab 5170  df-xp 5644  df-rel 5645  df-co 5647

This theorem is referenced by:  cotrg  6080  cotrgOLD  6081  cotrgOLDOLD  6082  dfco2  6218  resco  6223  coeq0  6228  coiun  6229  cocnvcnv2  6231  cores2  6232  co02  6233  co01  6234  coi1  6235  coass  6238  cossxp  6245  dfpo2  6269  fmptco  7101  cofunexg  7927  dftpos4  8224  ttrcltr  9669  ttrclco  9671  wunco  10686  relexprelg  15004  relexpaddg  15019  imasless  17503  znleval  21464  metustexhalf  24444  fcoinver  32533  fmptcof2  32581  cnvco1  35746  cnvco2  35747  opelco3  35762  txpss3v  35866  sscoid  35901  xrnss3v  38354  cononrel1  43583  cononrel2  43584  coiun1  43641  relexpaddss  43707  brco2f1o  44021  brco3f1o  44022  neicvgnvor  44105  sblpnf  44299  coxp  48821  xpco2  48845