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 ( 𝐴 ∘ 𝐵 )