Theorem relco 6111

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

Syntax hints:   ∧ wa 400  ∃wex 1806   class class class wbr 5113   ∘ ccom 5666  Rel wrel 5667

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-ss 3930  df-opab 5178  df-xp 5668  df-rel 5669  df-co 5671

This theorem is referenced by:  cotrg  6112  dfco2  6247  resco  6252  coeq0  6258  coiun  6259  cocnvcnv2  6261  cores2  6262  co02  6263  co01  6264  coi1  6265  coass  6268  cossxp  6274  dfpo2  6298  fmptco  7126  cofunexg  7946  dftpos4  8241  ttrcltr  9685  ttrclco  9687  wunco  10718  relexprelg  15075  relexpaddg  15090  imasless  17594  znleval  21673  metustexhalf  24682  fcoinver  32890  fmptcof2  32943  cnvco1  36150  cnvco2  36151  opelco3  36166  txpss3v  36267  sscoid  36302  xrnss3v  38920  cononrel1  44212  cononrel2  44213  coiun1  44270  relexpaddss  44336  brco2f1o  44650  brco3f1o  44651  neicvgnvor  44734  sblpnf  44912  coxp  49496  xpco2  49520