Theorem elopab

Description: Membership in a class abstraction of ordered pairs. (Contributed by NM, 24-Mar-1998)

	Ref	Expression
Assertion	elopab	$$⊢A\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \exists x\exists y\left(A=⟨x,y⟩\wedge \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		elex	$$⊢A\in \left\{⟨x,y⟩|\phi \right\}\to A\in \mathrm{V}$$
2		opex	$$⊢⟨x,y⟩\in \mathrm{V}$$
3		eleq1	$$⊢A=⟨x,y⟩\to \left(A\in \mathrm{V}\leftrightarrow ⟨x,y⟩\in \mathrm{V}\right)$$
4	2 3	mpbiri	$$⊢A=⟨x,y⟩\to A\in \mathrm{V}$$
5	4	adantr	$$⊢\left(A=⟨x,y⟩\wedge \phi \right)\to A\in \mathrm{V}$$
6	5	exlimivv	$$⊢\exists x\exists y\left(A=⟨x,y⟩\wedge \phi \right)\to A\in \mathrm{V}$$
7		elopabw	$$⊢A\in \mathrm{V}\to \left(A\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \exists x\exists y\left(A=⟨x,y⟩\wedge \phi \right)\right)$$
8	1 6 7	pm5.21nii	$$⊢A\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \exists x\exists y\left(A=⟨x,y⟩\wedge \phi \right)$$