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		eqeq1	$$⊢z=w\to \left(z=⟨x,y⟩\leftrightarrow w=⟨x,y⟩\right)$$
8	7	anbi1d	$$⊢z=w\to \left(\left(z=⟨x,y⟩\wedge \phi \right)\leftrightarrow \left(w=⟨x,y⟩\wedge \phi \right)\right)$$
9	8	2exbidv	$$⊢z=w\to \left(\exists x\exists y\left(z=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\right)$$
10		eqeq1	$$⊢w=A\to \left(w=⟨x,y⟩\leftrightarrow A=⟨x,y⟩\right)$$
11	10	anbi1d	$$⊢w=A\to \left(\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \left(A=⟨x,y⟩\wedge \phi \right)\right)$$
12	11	2exbidv	$$⊢w=A\to \left(\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists x\exists y\left(A=⟨x,y⟩\wedge \phi \right)\right)$$
13		df-opab	$$⊢\left\{⟨x,y⟩|\phi \right\}=\left\{z|\exists x\exists y\left(z=⟨x,y⟩\wedge \phi \right)\right\}$$
14	9 12 13	elab2gw	$$⊢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)$$
15	1 6 14	pm5.21nii	$$⊢A\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \exists x\exists y\left(A=⟨x,y⟩\wedge \phi \right)$$