Theorem relco 6097

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

Syntax hints:   ∧ wa 399  ∃wex 1799   class class class wbr 5100   ∘ ccom 5651  Rel wrel 5652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-ss 3921  df-opab 5163  df-xp 5653  df-rel 5654  df-co 5656

This theorem is referenced by:  cotrg  6098  dfco2  6232  resco  6237  coeq0  6243  coiun  6244  cocnvcnv2  6246  cores2  6247  co02  6248  co01  6249  coi1  6250  coass  6253  cossxp  6259  dfpo2  6283  fmptco  7111  cofunexg  7930  dftpos4  8225  ttrcltr  9671  ttrclco  9673  wunco  10691  relexprelg  15051  relexpaddg  15066  imasless  17570  znleval  21606  metustexhalf  24616  fcoinver  32804  fmptcof2  32859  cnvco1  36109  cnvco2  36110  opelco3  36125  txpss3v  36226  sscoid  36261  xrnss3v  38880  cononrel1  44170  cononrel2  44171  coiun1  44228  relexpaddss  44294  brco2f1o  44608  brco3f1o  44609  neicvgnvor  44692  sblpnf  44886  coxp  49454  xpco2  49478