Theorem relcnv

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

	Ref	Expression
Assertion	relcnv	⊢ Rel ◡ 𝐴

Proof

Step	Hyp	Ref	Expression
1		df-cnv	⊢ ◡ 𝐴 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦 𝐴 𝑥 }
2	1	relopabiv	⊢ Rel ◡ 𝐴