Theorem relco

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

	Ref	Expression
Assertion	relco	$$⊢\mathrm{Rel}\left(A\circ B\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-co	$$⊢A\circ B=\left\{⟨x,y⟩|\exists z\left(xBz\wedge zAy\right)\right\}$$
2	1	relopabi	$$⊢\mathrm{Rel}\left(A\circ B\right)$$