Theorem relco 6121

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

Syntax hints:   ∧ wa 394  ∃wex 1774   class class class wbr 5154   ∘ ccom 5688  Rel wrel 5689

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-ext 2700

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2062  df-clab 2707  df-cleq 2721  df-clel 2806  df-v 3474  df-ss 3975  df-opab 5217  df-xp 5690  df-rel 5691  df-co 5693

This theorem is referenced by:  cotrg  6122  cotrgOLD  6123  cotrgOLDOLD  6124  dfco2  6259  resco  6264  coeq0  6269  coiun  6270  cocnvcnv2  6272  cores2  6273  co02  6274  co01  6275  coi1  6276  coass  6279  cossxp  6286  dfpo2  6310  fmptco  7145  cofunexg  7967  dftpos4  8264  ttrcltr  9760  ttrclco  9762  wunco  10777  relexprelg  15056  relexpaddg  15071  imasless  17568  znleval  21564  metustexhalf  24556  fcoinver  32570  fmptcof2  32620  cnvco1  35666  cnvco2  35667  opelco3  35683  txpss3v  35787  sscoid  35822  xrnss3v  38155  cononrel1  43373  cononrel2  43374  coiun1  43431  relexpaddss  43497  brco2f1o  43811  brco3f1o  43812  neicvgnvor  43895  sblpnf  44096