Theorem relco 6148

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

Syntax hints:   ∧ wa 396  ∃wex 1782   class class class wbr 5074   ∘ ccom 5593  Rel wrel 5594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-opab 5137  df-xp 5595  df-rel 5596  df-co 5598

This theorem is referenced by:  dfco2  6149  resco  6154  coeq0  6159  coiun  6160  cocnvcnv2  6162  cores2  6163  co02  6164  co01  6165  coi1  6166  coass  6169  cossxp  6175  dfpo2  6199  dffun2  6443  fmptco  7001  cofunexg  7791  dftpos4  8061  ttrcltr  9474  ttrclco  9476  wunco  10489  relexprelg  14749  relexpaddg  14764  imasless  17251  znleval  20762  metustexhalf  23712  fcoinver  30946  fmptcof2  30994  cnvco1  33726  cnvco2  33727  opelco3  33749  txpss3v  34180  sscoid  34215  xrnss3v  36502  cononrel1  41202  cononrel2  41203  coiun1  41260  relexpaddss  41326  brco2f1o  41642  brco3f1o  41643  neicvgnvor  41726  sblpnf  41928