Theorem relco 5979

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

Syntax hints:   ∧ wa 396  ∃wex 1765   class class class wbr 4968   ∘ ccom 5454  Rel wrel 5455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-rab 3116  df-v 3442  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-sn 4479  df-pr 4481  df-op 4485  df-opab 5031  df-xp 5456  df-rel 5457  df-co 5459

This theorem is referenced by:  dfco2  5980  resco  5985  coeq0  5990  coiun  5991  cocnvcnv2  5993  cores2  5994  co02  5995  co01  5996  coi1  5997  coass  6000  cossxp  6005  fmptco  6761  cofunexg  7513  dftpos4  7769  wunco  10008  relexprelg  14235  relexpaddg  14250  imasless  16646  znleval  20387  metustexhalf  22853  fcoinver  30043  fmptcof2  30088  dfpo2  32601  cnvco1  32605  cnvco2  32606  opelco3  32628  txpss3v  32950  sscoid  32985  xrnss3v  35176  cononrel1  39460  cononrel2  39461  coiun1  39503  relexpaddss  39569  brco2f1o  39888  brco3f1o  39889  neicvgnvor  39972  sblpnf  40201