Theorem relco 6067

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

Syntax hints:   ∧ wa 395  ∃wex 1780   class class class wbr 5098   ∘ ccom 5628  Rel wrel 5629

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-ss 3918  df-opab 5161  df-xp 5630  df-rel 5631  df-co 5633

This theorem is referenced by:  cotrg  6068  dfco2  6203  resco  6208  coeq0  6214  coiun  6215  cocnvcnv2  6217  cores2  6218  co02  6219  co01  6220  coi1  6221  coass  6224  cossxp  6230  dfpo2  6254  fmptco  7074  cofunexg  7893  dftpos4  8187  ttrcltr  9625  ttrclco  9627  wunco  10644  relexprelg  14961  relexpaddg  14976  imasless  17461  znleval  21509  metustexhalf  24500  fcoinver  32679  fmptcof2  32735  cnvco1  35953  cnvco2  35954  opelco3  35969  txpss3v  36070  sscoid  36105  xrnss3v  38576  cononrel1  43845  cononrel2  43846  coiun1  43903  relexpaddss  43969  brco2f1o  44283  brco3f1o  44284  neicvgnvor  44367  sblpnf  44561  coxp  49088  xpco2  49112