Theorem relco 6068

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

Syntax hints:   ∧ wa 395  ∃wex 1779   class class class wbr 5102   ∘ ccom 5635  Rel wrel 5636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-ss 3928  df-opab 5165  df-xp 5637  df-rel 5638  df-co 5640

This theorem is referenced by:  cotrg  6069  cotrgOLD  6070  dfco2  6206  resco  6211  coeq0  6216  coiun  6217  cocnvcnv2  6219  cores2  6220  co02  6221  co01  6222  coi1  6223  coass  6226  cossxp  6233  dfpo2  6257  fmptco  7083  cofunexg  7907  dftpos4  8201  ttrcltr  9645  ttrclco  9647  wunco  10662  relexprelg  14980  relexpaddg  14995  imasless  17479  znleval  21440  metustexhalf  24420  fcoinver  32506  fmptcof2  32554  cnvco1  35719  cnvco2  35720  opelco3  35735  txpss3v  35839  sscoid  35874  xrnss3v  38327  cononrel1  43556  cononrel2  43557  coiun1  43614  relexpaddss  43680  brco2f1o  43994  brco3f1o  43995  neicvgnvor  44078  sblpnf  44272  coxp  48794  xpco2  48818