Theorem relco 6078

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

Syntax hints:   ∧ wa 399  ∃wex 1781   class class class wbr 5035   ∘ ccom 5531  Rel wrel 5532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3867  df-ss 3877  df-opab 5098  df-xp 5533  df-rel 5534  df-co 5536

This theorem is referenced by:  dfco2  6079  resco  6084  coeq0  6089  coiun  6090  cocnvcnv2  6092  cores2  6093  co02  6094  co01  6095  coi1  6096  coass  6099  cossxp  6105  fmptco  6887  cofunexg  7659  dftpos4  7926  wunco  10198  relexprelg  14450  relexpaddg  14465  imasless  16876  znleval  20327  metustexhalf  23263  fcoinver  30473  fmptcof2  30522  dfpo2  33242  cnvco1  33246  cnvco2  33247  opelco3  33269  txpss3v  33755  sscoid  33790  xrnss3v  36090  cononrel1  40695  cononrel2  40696  coiun1  40754  relexpaddss  40820  brco2f1o  41136  brco3f1o  41137  neicvgnvor  41220  sblpnf  41415