Theorem relco 6122

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

This proof depends on syntax axioms:   ∧ wa 401  ∃wex 1812   class class class wbr 5108   ∘ ccom 5662  Rel wrel 5663

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-opab 5174  df-xp 5664  df-rel 5665  df-co 5667

This theorem is used by:  cotrg  6123  dfco2  6265  resco  6270  coeq0  6276  coiun  6277  cocnvcnv2  6279  cores2  6280  co02  6283  co01  6284  coi1  6285  coass  6290  coassOLD  6291  cossxp  6298  dfpo2  6325  fmptco  7162  cofunexg  7995  dftpos4  8300  ttrcltr  9754  ttrclco  9756  wunco  10857  relexprelg  15234  relexpaddg  15249  imasless  17762  znleval  21915  metustexhalf  24930  fcoinver  33296  fmptcof2  33349  cnvco1  36739  cnvco2  36740  opelco3  36754  txpss3v  36855  sscoid  36890  comodular  38207  xrnss3v  39579  cononrel1  44855  cononrel2  44856  coiun1  44913  relexpaddss  44979  brco2f1o  45293  brco3f1o  45294  neicvgnvor  45377  sblpnf  45555  cocanss1  46185  hfstructhf  46297  coxp  50275  xpco2  50299