Theorem relco 6060

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

Syntax hints:   ∧ wa 396  ∃wex 1786   class class class wbr 5072   ∘ ccom 5622  Rel wrel 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-ss 3900  df-opab 5135  df-xp 5624  df-rel 5625  df-co 5627

This theorem is referenced by:  cotrg  6061  dfco2  6196  resco  6201  coeq0  6207  coiun  6208  cocnvcnv2  6210  cores2  6211  co02  6212  co01  6213  coi1  6214  coass  6217  cossxp  6223  dfpo2  6247  fmptco  7071  cofunexg  7891  dftpos4  8185  ttrcltr  9628  ttrclco  9630  wunco  10647  relexprelg  14991  relexpaddg  15006  imasless  17495  znleval  21529  metustexhalf  24539  fcoinver  32693  fmptcof2  32749  cnvco1  35987  cnvco2  35988  opelco3  36003  txpss3v  36104  sscoid  36139  xrnss3v  38748  cononrel1  44038  cononrel2  44039  coiun1  44096  relexpaddss  44162  brco2f1o  44476  brco3f1o  44477  neicvgnvor  44560  sblpnf  44754  coxp  49323  xpco2  49347