Theorem relco 6110

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

Syntax hints:   ∧ wa 400  ∃wex 1809   class class class wbr 5109   ∘ ccom 5665  Rel wrel 5666

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3922  df-opab 5174  df-xp 5667  df-rel 5668  df-co 5670

This theorem is referenced by:  cotrg  6111  dfco2  6246  resco  6251  coeq0  6257  coiun  6258  cocnvcnv2  6260  cores2  6261  co02  6262  co01  6263  coi1  6264  coass  6267  cossxp  6273  dfpo2  6297  fmptco  7125  cofunexg  7942  dftpos4  8237  ttrcltr  9681  ttrclco  9683  wunco  10713  relexprelg  15071  relexpaddg  15086  imasless  17589  znleval  21704  metustexhalf  24713  fcoinver  32949  fmptcof2  33002  cnvco1  36251  cnvco2  36252  opelco3  36267  txpss3v  36368  sscoid  36403  xrnss3v  39050  cononrel1  44340  cononrel2  44341  coiun1  44398  relexpaddss  44464  brco2f1o  44778  brco3f1o  44779  neicvgnvor  44862  sblpnf  45040  coxp  49631  xpco2  49655