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

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

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-opab 5168  df-xp 5657  df-rel 5658  df-co 5660

This theorem is used by:  cotrg  6105  dfco2  6246  resco  6251  coeq0  6257  coiun  6258  cocnvcnv2  6260  cores2  6261  co02  6262  co01  6263  coi1  6264  coass  6267  cossxp  6274  dfpo2  6299  fmptco  7130  cofunexg  7961  dftpos4  8262  ttrcltr  9717  ttrclco  9719  wunco  10818  relexprelg  15191  relexpaddg  15206  imasless  17712  znleval  21860  metustexhalf  24875  fcoinver  33198  fmptcof2  33251  cnvco1  36524  cnvco2  36525  opelco3  36539  txpss3v  36640  sscoid  36675  xrnss3v  39313  cononrel1  44593  cononrel2  44594  coiun1  44651  relexpaddss  44717  brco2f1o  45031  brco3f1o  45032  neicvgnvor  45115  sblpnf  45293  cocanss1  45923  hfstructhf  46029  coxp  49942  xpco2  49966