Theorem opabn0

Description: Nonempty ordered pair class abstraction. (Contributed by NM, 10-Oct-2007)

	Ref	Expression
Assertion	opabn0	$$⊢\left\{⟨x,y⟩|\phi \right\}\ne \varnothing \leftrightarrow \exists x\exists y\phi$$

Proof

Step	Hyp	Ref	Expression
1		n0	$$⊢\left\{⟨x,y⟩|\phi \right\}\ne \varnothing \leftrightarrow \exists zz\in \left\{⟨x,y⟩|\phi \right\}$$
2		elopab	$$⊢z\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \exists x\exists y\left(z=⟨x,y⟩\wedge \phi \right)$$
3	2	exbii	$$⊢\exists zz\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \exists z\exists x\exists y\left(z=⟨x,y⟩\wedge \phi \right)$$
4		exrot3	$$⊢\exists z\exists x\exists y\left(z=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists x\exists y\exists z\left(z=⟨x,y⟩\wedge \phi \right)$$
5		opex	$$⊢⟨x,y⟩\in \mathrm{V}$$
6	5	isseti	$$⊢\exists zz=⟨x,y⟩$$
7		19.41v	$$⊢\exists z\left(z=⟨x,y⟩\wedge \phi \right)\leftrightarrow \left(\exists zz=⟨x,y⟩\wedge \phi \right)$$
8	6 7	mpbiran	$$⊢\exists z\left(z=⟨x,y⟩\wedge \phi \right)\leftrightarrow \phi$$
9	8	2exbii	$$⊢\exists x\exists y\exists z\left(z=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists x\exists y\phi$$
10	4 9	bitri	$$⊢\exists z\exists x\exists y\left(z=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists x\exists y\phi$$
11	3 10	bitri	$$⊢\exists zz\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \exists x\exists y\phi$$
12	1 11	bitri	$$⊢\left\{⟨x,y⟩|\phi \right\}\ne \varnothing \leftrightarrow \exists x\exists y\phi$$