Theorem relco 6056

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

Syntax hints:   ∧ wa 395  ∃wex 1780   class class class wbr 5089   ∘ ccom 5618  Rel wrel 5619

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3914  df-opab 5152  df-xp 5620  df-rel 5621  df-co 5623

This theorem is referenced by:  cotrg  6057  dfco2  6192  resco  6197  coeq0  6203  coiun  6204  cocnvcnv2  6206  cores2  6207  co02  6208  co01  6209  coi1  6210  coass  6213  cossxp  6219  dfpo2  6243  fmptco  7062  cofunexg  7881  dftpos4  8175  ttrcltr  9606  ttrclco  9608  wunco  10624  relexprelg  14945  relexpaddg  14960  imasless  17444  znleval  21491  metustexhalf  24471  fcoinver  32584  fmptcof2  32639  cnvco1  35803  cnvco2  35804  opelco3  35819  txpss3v  35920  sscoid  35955  xrnss3v  38415  cononrel1  43697  cononrel2  43698  coiun1  43755  relexpaddss  43821  brco2f1o  44135  brco3f1o  44136  neicvgnvor  44219  sblpnf  44413  coxp  48943  xpco2  48967