Theorem 0nelopab

Description: The empty set is never an element in an ordered-pair class abstraction. (Contributed by Alexander van der Vekens, 5-Nov-2017) Reduce axiom usage and shorten proof. (Revised by GG, 3-Oct-2024)

	Ref	Expression
Assertion	0nelopab	$$⊢\neg \varnothing \in \left\{⟨x,y⟩|\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢x\in \mathrm{V}$$
2		vex	$$⊢y\in \mathrm{V}$$
3	1 2	opnzi	$$⊢⟨x,y⟩\ne \varnothing$$
4	3	nesymi	$$⊢\neg \varnothing =⟨x,y⟩$$
5	4	intnanr	$$⊢\neg \left(\varnothing =⟨x,y⟩\wedge \phi \right)$$
6	5	nex	$$⊢\neg \exists y\left(\varnothing =⟨x,y⟩\wedge \phi \right)$$
7	6	nex	$$⊢\neg \exists x\exists y\left(\varnothing =⟨x,y⟩\wedge \phi \right)$$
8		elopab	$$⊢\varnothing \in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \exists x\exists y\left(\varnothing =⟨x,y⟩\wedge \phi \right)$$
9	7 8	mtbir	$$⊢\neg \varnothing \in \left\{⟨x,y⟩|\phi \right\}$$