Theorem relco 6112

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

This proof depends on syntax axioms:   ∧ wa 401  ∃wex 1812   class class class wbr 5111   ∘ ccom 5667  Rel wrel 5668

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3923  df-opab 5176  df-xp 5669  df-rel 5670  df-co 5672

This theorem is used by:  cotrg  6113  dfco2  6248  resco  6253  coeq0  6259  coiun  6260  cocnvcnv2  6262  cores2  6263  co02  6264  co01  6265  coi1  6266  coass  6269  cossxp  6276  dfpo2  6301  fmptco  7129  cofunexg  7952  dftpos4  8247  ttrcltr  9692  ttrclco  9694  wunco  10735  relexprelg  15101  relexpaddg  15116  imasless  17618  znleval  21756  metustexhalf  24766  fcoinver  33022  fmptcof2  33075  cnvco1  36290  cnvco2  36291  opelco3  36306  txpss3v  36407  sscoid  36442  xrnss3v  39090  cononrel1  44380  cononrel2  44381  coiun1  44438  relexpaddss  44504  brco2f1o  44818  brco3f1o  44819  neicvgnvor  44902  sblpnf  45080  coxp  49670  xpco2  49694