Theorem elcnv2

Description: Membership in a converse relation. Equation 5 of Suppes p. 62. (Contributed by NM, 11-Aug-2004)

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

Proof

Step	Hyp	Ref	Expression
1		elcnv	$$⊢A\in R^{-1}\leftrightarrow \exists x\exists y\left(A=⟨x,y⟩\wedge yRx\right)$$
2		df-br	$$⊢yRx\leftrightarrow ⟨y,x⟩\in R$$
3	2	anbi2i	$$⊢\left(A=⟨x,y⟩\wedge yRx\right)\leftrightarrow \left(A=⟨x,y⟩\wedge ⟨y,x⟩\in R\right)$$
4	3	2exbii	$$⊢\exists x\exists y\left(A=⟨x,y⟩\wedge yRx\right)\leftrightarrow \exists x\exists y\left(A=⟨x,y⟩\wedge ⟨y,x⟩\in R\right)$$
5	1 4	bitri	$$⊢A\in R^{-1}\leftrightarrow \exists x\exists y\left(A=⟨x,y⟩\wedge ⟨y,x⟩\in R\right)$$