Theorem relco 6104

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

This proof depends on syntax axioms:   ∧ wa 401  ∃wex 1812   class class class wbr 5103   ∘ ccom 5659  Rel wrel 5660

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 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3916  df-opab 5168  df-xp 5661  df-rel 5662  df-co 5664

This theorem is used by:  cotrg  6105  dfco2  6241  resco  6246  coeq0  6252  coiun  6253  cocnvcnv2  6255  cores2  6256  co02  6257  co01  6258  coi1  6259  coass  6262  cossxp  6269  dfpo2  6294  fmptco  7124  cofunexg  7947  dftpos4  8244  ttrcltr  9696  ttrclco  9698  wunco  10743  relexprelg  15112  relexpaddg  15127  imasless  17627  znleval  21768  metustexhalf  24783  fcoinver  33078  fmptcof2  33131  cnvco1  36339  cnvco2  36340  opelco3  36355  txpss3v  36456  sscoid  36491  xrnss3v  39130  cononrel1  44435  cononrel2  44436  coiun1  44493  relexpaddss  44559  brco2f1o  44873  brco3f1o  44874  neicvgnvor  44957  sblpnf  45135  coxp  49762  xpco2  49786