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 ( A o. B )

Proof

Step Hyp Ref Expression
1 df-co 
 |-  ( A o. B ) = { <. x , y >. | E. z ( x B z /\ z A y ) }
2 1 relopabiv 
 |-  Rel ( A o. B )