Theorem relco 6106

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

This proof depends on syntax axioms:   ∧ wa 401  ∃wex 1811   class class class wbr 5102   ∘ ccom 5655  Rel wrel 5656

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3897  df-opab 5167  df-xp 5657  df-rel 5658  df-co 5660

This theorem is used by:  cotrg  6107  dfco2  6249  resco  6254  coeq0  6260  coiun  6261  cocnvcnv2  6263  cores2  6264  co02  6265  co01  6266  coi1  6267  coass  6270  cossxp  6277  dfpo2  6302  fmptco  7135  cofunexg  7965  dftpos4  8270  ttrcltr  9724  ttrclco  9726  wunco  10825  relexprelg  15200  relexpaddg  15215  imasless  17721  znleval  21869  metustexhalf  24884  fcoinver  33249  fmptcof2  33302  cnvco1  36648  cnvco2  36649  opelco3  36663  txpss3v  36764  sscoid  36799  xrnss3v  39450  cononrel1  44731  cononrel2  44732  coiun1  44789  relexpaddss  44855  brco2f1o  45169  brco3f1o  45170  neicvgnvor  45253  sblpnf  45431  cocanss1  46060  hfstructhf  46166  coxp  50080  xpco2  50104