Theorem relco 6065

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

Syntax hints:   ∧ wa 395  ∃wex 1780   class class class wbr 5096   ∘ ccom 5626  Rel wrel 5627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-ss 3916  df-opab 5159  df-xp 5628  df-rel 5629  df-co 5631

This theorem is referenced by:  cotrg  6066  dfco2  6201  resco  6206  coeq0  6212  coiun  6213  cocnvcnv2  6215  cores2  6216  co02  6217  co01  6218  coi1  6219  coass  6222  cossxp  6228  dfpo2  6252  fmptco  7072  cofunexg  7891  dftpos4  8185  ttrcltr  9623  ttrclco  9625  wunco  10642  relexprelg  14959  relexpaddg  14974  imasless  17459  znleval  21507  metustexhalf  24498  fcoinver  32628  fmptcof2  32684  cnvco1  35902  cnvco2  35903  opelco3  35918  txpss3v  36019  sscoid  36054  xrnss3v  38505  cononrel1  43777  cononrel2  43778  coiun1  43835  relexpaddss  43901  brco2f1o  44215  brco3f1o  44216  neicvgnvor  44299  sblpnf  44493  coxp  49020  xpco2  49044