Theorem relco 5671

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

Syntax hints:   ∧ wa 383  ∃wex 1744   class class class wbr 4685   ∘ ccom 5147  Rel wrel 5148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-opab 4746  df-xp 5149  df-rel 5150  df-co 5152

This theorem is referenced by:  dfco2  5672  resco  5677  coeq0  5682  coiun  5683  cocnvcnv2  5685  cores2  5686  co02  5687  co01  5688  coi1  5689  coass  5692  cossxp  5696  fmptco  6436  cofunexg  7172  dftpos4  7416  wunco  9593  relexprelg  13822  relexpaddg  13837  imasless  16247  znleval  19951  metustexhalf  22408  fcoinver  29544  fmptcof2  29585  dfpo2  31771  cnvco1  31775  cnvco2  31776  opelco3  31802  txpss3v  32110  sscoid  32145  xrnss3v  34274  cononrel1  38217  cononrel2  38218  coiun1  38261  relexpaddss  38327  brco2f1o  38647  brco3f1o  38648  neicvgnvor  38731  sblpnf  38826