Theorem elopabrOLD

Description: Obsolete version of elopabr as of 11-Dec-2024. (Contributed by AV, 16-Feb-2021) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	elopabrOLD	$$⊢A\in \left\{⟨x,y⟩|xRy\right\}\to A\in R$$

Proof

Step	Hyp	Ref	Expression
1		elopab	$$⊢A\in \left\{⟨x,y⟩|xRy\right\}\leftrightarrow \exists x\exists y\left(A=⟨x,y⟩\wedge xRy\right)$$
2		df-br	$$⊢xRy\leftrightarrow ⟨x,y⟩\in R$$
3	2	biimpi	$$⊢xRy\to ⟨x,y⟩\in R$$
4		eleq1	$$⊢A=⟨x,y⟩\to \left(A\in R\leftrightarrow ⟨x,y⟩\in R\right)$$
5	3 4	imbitrrid	$$⊢A=⟨x,y⟩\to \left(xRy\to A\in R\right)$$
6	5	imp	$$⊢\left(A=⟨x,y⟩\wedge xRy\right)\to A\in R$$
7	6	exlimivv	$$⊢\exists x\exists y\left(A=⟨x,y⟩\wedge xRy\right)\to A\in R$$
8	1 7	sylbi	$$⊢A\in \left\{⟨x,y⟩|xRy\right\}\to A\in R$$