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