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  21496  metustexhalf  24477  fcoinver  32583  fmptcof2  32631  cnvco1  35739  cnvco2  35740  opelco3  35755  txpss3v  35859  sscoid  35894  xrnss3v  38347  cononrel1  43576  cononrel2  43577  coiun1  43634  relexpaddss  43700  brco2f1o  44014  brco3f1o  44015  neicvgnvor  44098  sblpnf  44292  coxp  48814  xpco2  48838