Theorem relco 6126

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

Syntax hints:   ∧ wa 395  ∃wex 1779   class class class wbr 5143   ∘ ccom 5689  Rel wrel 5690

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-opab 5206  df-xp 5691  df-rel 5692  df-co 5694

This theorem is referenced by:  cotrg  6127  cotrgOLD  6128  cotrgOLDOLD  6129  dfco2  6265  resco  6270  coeq0  6275  coiun  6276  cocnvcnv2  6278  cores2  6279  co02  6280  co01  6281  coi1  6282  coass  6285  cossxp  6292  dfpo2  6316  fmptco  7149  cofunexg  7973  dftpos4  8270  ttrcltr  9756  ttrclco  9758  wunco  10773  relexprelg  15077  relexpaddg  15092  imasless  17585  znleval  21573  metustexhalf  24569  fcoinver  32617  fmptcof2  32667  cnvco1  35759  cnvco2  35760  opelco3  35775  txpss3v  35879  sscoid  35914  xrnss3v  38373  cononrel1  43607  cononrel2  43608  coiun1  43665  relexpaddss  43731  brco2f1o  44045  brco3f1o  44046  neicvgnvor  44129  sblpnf  44329  coxp  48744