Theorem elcnv

Description: Membership in a converse relation. Equation 5 of Suppes p. 62. (Contributed by NM, 24-Mar-1998)

	Ref	Expression
Assertion	elcnv	$$⊢A\in R^{-1}\leftrightarrow \exists x\exists y\left(A=⟨x,y⟩\wedge yRx\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-cnv	$$⊢R^{-1}=\left\{⟨x,y⟩|yRx\right\}$$
2	1	eleq2i	$$⊢A\in R^{-1}\leftrightarrow A\in \left\{⟨x,y⟩|yRx\right\}$$
3		elopab	$$⊢A\in \left\{⟨x,y⟩|yRx\right\}\leftrightarrow \exists x\exists y\left(A=⟨x,y⟩\wedge yRx\right)$$
4	2 3	bitri	$$⊢A\in R^{-1}\leftrightarrow \exists x\exists y\left(A=⟨x,y⟩\wedge yRx\right)$$