Theorem relco 6105

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

Syntax hints:   ∧ wa 397  ∃wex 1782   class class class wbr 5148   ∘ ccom 5680  Rel wrel 5681

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3955  df-ss 3965  df-opab 5211  df-xp 5682  df-rel 5683  df-co 5685

This theorem is referenced by:  cotrg  6106  cotrgOLD  6107  cotrgOLDOLD  6108  dfco2  6242  resco  6247  coeq0  6252  coiun  6253  cocnvcnv2  6255  cores2  6256  co02  6257  co01  6258  coi1  6259  coass  6262  cossxp  6269  dfpo2  6293  fmptco  7124  cofunexg  7932  dftpos4  8227  ttrcltr  9708  ttrclco  9710  wunco  10725  relexprelg  14982  relexpaddg  14997  imasless  17483  znleval  21102  metustexhalf  24057  fcoinver  31823  fmptcof2  31870  cnvco1  34718  cnvco2  34719  opelco3  34735  txpss3v  34839  sscoid  34874  xrnss3v  37231  cononrel1  42331  cononrel2  42332  coiun1  42389  relexpaddss  42455  brco2f1o  42769  brco3f1o  42770  neicvgnvor  42853  sblpnf  43055