Theorem relco 6092

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

Syntax hints:   ∧ wa 398  ∃wex 1776   class class class wbr 5059   ∘ ccom 5554  Rel wrel 5555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3497  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4562  df-pr 4564  df-op 4568  df-opab 5122  df-xp 5556  df-rel 5557  df-co 5559

This theorem is referenced by:  dfco2  6093  resco  6098  coeq0  6103  coiun  6104  cocnvcnv2  6106  cores2  6107  co02  6108  co01  6109  coi1  6110  coass  6113  cossxp  6118  fmptco  6886  cofunexg  7644  dftpos4  7905  wunco  10149  relexprelg  14391  relexpaddg  14406  imasless  16807  znleval  20695  metustexhalf  23160  fcoinver  30351  fmptcof2  30396  dfpo2  32986  cnvco1  32990  cnvco2  32991  opelco3  33013  txpss3v  33334  sscoid  33369  xrnss3v  35618  cononrel1  39947  cononrel2  39948  coiun1  39990  relexpaddss  40056  brco2f1o  40375  brco3f1o  40376  neicvgnvor  40459  sblpnf  40635