Theorem relco 5633

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

Syntax hints:   ∧ wa 384  ∃wex 1704   class class class wbr 4653   ∘ ccom 5118  Rel wrel 5119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-opab 4713  df-xp 5120  df-rel 5121  df-co 5123

This theorem is referenced by:  dfco2  5634  resco  5639  coeq0  5644  coiun  5645  cocnvcnv2  5647  cores2  5648  co02  5649  co01  5650  coi1  5651  coass  5654  cossxp  5658  fmptco  6396  cofunexg  7130  dftpos4  7371  wunco  9555  relexprelg  13778  relexpaddg  13793  imasless  16200  znleval  19903  metustexhalf  22361  fcoinver  29418  fmptcof2  29457  dfpo2  31645  cnvco1  31649  cnvco2  31650  opelco3  31678  txpss3v  31985  sscoid  32020  xrnss3v  34135  cononrel1  37900  cononrel2  37901  coiun1  37944  relexpaddss  38010  brco2f1o  38330  brco3f1o  38331  neicvgnvor  38414  sblpnf  38509