Theorem relco 6059

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

Syntax hints:   ∧ wa 395  ∃wex 1779   class class class wbr 5092   ∘ ccom 5623  Rel wrel 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-ss 3920  df-opab 5155  df-xp 5625  df-rel 5626  df-co 5628

This theorem is referenced by:  cotrg  6060  dfco2  6194  resco  6199  coeq0  6204  coiun  6205  cocnvcnv2  6207  cores2  6208  co02  6209  co01  6210  coi1  6211  coass  6214  cossxp  6220  dfpo2  6244  fmptco  7063  cofunexg  7884  dftpos4  8178  ttrcltr  9612  ttrclco  9614  wunco  10627  relexprelg  14945  relexpaddg  14960  imasless  17444  znleval  21461  metustexhalf  24442  fcoinver  32548  fmptcof2  32600  cnvco1  35736  cnvco2  35737  opelco3  35752  txpss3v  35856  sscoid  35891  xrnss3v  38344  cononrel1  43571  cononrel2  43572  coiun1  43629  relexpaddss  43695  brco2f1o  44009  brco3f1o  44010  neicvgnvor  44093  sblpnf  44287  coxp  48821  xpco2  48845