Metamath Proof Explorer


Theorem relco

Description: A composition is a relation. Exercise 24 of TakeutiZaring p. 25. (Contributed by NM, 26-Jan-1997)

Ref Expression
Assertion relco Rel ( 𝐴𝐵 )

Proof

Step Hyp Ref Expression
1 df-co ( 𝐴𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ( 𝑥 𝐵 𝑧𝑧 𝐴 𝑦 ) }
2 1 relopabiv Rel ( 𝐴𝐵 )