Theorem elopabr

Description: Membership in an ordered-pair class abstraction defined by a binary relation. (Contributed by AV, 16-Feb-2021)

	Ref	Expression
Assertion	elopabr	$$⊢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	syl5ibr	$$⊢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$$