Theorem relco 6128

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

Syntax hints:   ∧ wa 395  ∃wex 1775   class class class wbr 5147   ∘ ccom 5692  Rel wrel 5693

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-ss 3979  df-opab 5210  df-xp 5694  df-rel 5695  df-co 5697

This theorem is referenced by:  cotrg  6129  cotrgOLD  6130  cotrgOLDOLD  6131  dfco2  6266  resco  6271  coeq0  6276  coiun  6277  cocnvcnv2  6279  cores2  6280  co02  6281  co01  6282  coi1  6283  coass  6286  cossxp  6293  dfpo2  6317  fmptco  7148  cofunexg  7971  dftpos4  8268  ttrcltr  9753  ttrclco  9755  wunco  10770  relexprelg  15073  relexpaddg  15088  imasless  17586  znleval  21590  metustexhalf  24584  fcoinver  32623  fmptcof2  32673  cnvco1  35738  cnvco2  35739  opelco3  35755  txpss3v  35859  sscoid  35894  xrnss3v  38353  cononrel1  43583  cononrel2  43584  coiun1  43641  relexpaddss  43707  brco2f1o  44021  brco3f1o  44022  neicvgnvor  44105  sblpnf  44305