Theorem relco 6095

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

Syntax hints:   ∧ wa 395  ∃wex 1779   class class class wbr 5119   ∘ ccom 5658  Rel wrel 5659

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-ss 3943  df-opab 5182  df-xp 5660  df-rel 5661  df-co 5663

This theorem is referenced by:  cotrg  6096  cotrgOLD  6097  cotrgOLDOLD  6098  dfco2  6234  resco  6239  coeq0  6244  coiun  6245  cocnvcnv2  6247  cores2  6248  co02  6249  co01  6250  coi1  6251  coass  6254  cossxp  6261  dfpo2  6285  fmptco  7119  cofunexg  7947  dftpos4  8244  ttrcltr  9730  ttrclco  9732  wunco  10747  relexprelg  15057  relexpaddg  15072  imasless  17554  znleval  21515  metustexhalf  24495  fcoinver  32585  fmptcof2  32635  cnvco1  35776  cnvco2  35777  opelco3  35792  txpss3v  35896  sscoid  35931  xrnss3v  38390  cononrel1  43618  cononrel2  43619  coiun1  43676  relexpaddss  43742  brco2f1o  44056  brco3f1o  44057  neicvgnvor  44140  sblpnf  44334  coxp  48811