Theorem relcnv

Description: A converse is a relation. Theorem 12 of Suppes p. 62. (Contributed by NM, 29-Oct-1996)

	Ref	Expression
Assertion	relcnv	$$⊢\mathrm{Rel}{A}^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		df-cnv	$$⊢A^{-1}=\left\{⟨x,y⟩|yAx\right\}$$
2	1	relopabi	$$⊢\mathrm{Rel}{A}^{-1}$$