Theorem noel

Description: The empty set has no elements. Theorem 6.14 of Quine p. 44. (Contributed by NM, 21-Jun-1993) (Proof shortened by Mario Carneiro, 1-Sep-2015) Remove dependency on ax-10 , ax-11 , and ax-12 . (Revised by Steven Nguyen, 3-May-2023) (Proof shortened by BJ, 23-Sep-2024)

	Ref	Expression
Assertion	noel	$$⊢\neg A\in \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		nsb	$$⊢\forall y\neg \perp \to \neg \left[x/y\right]\perp$$
2		fal	$$⊢\neg \perp$$
3	1 2	mpg	$$⊢\neg \left[x/y\right]\perp$$
4		dfnul4	$$⊢\varnothing =\left\{y|\perp \right\}$$
5	4	eleq2i	$$⊢x\in \varnothing \leftrightarrow x\in \left\{y|\perp \right\}$$
6		df-clab	$$⊢x\in \left\{y|\perp \right\}\leftrightarrow \left[x/y\right]\perp$$
7	5 6	bitri	$$⊢x\in \varnothing \leftrightarrow \left[x/y\right]\perp$$
8	3 7	mtbir	$$⊢\neg x\in \varnothing$$
9	8	intnan	$$⊢\neg \left(x=A\wedge x\in \varnothing \right)$$
10	9	nex	$$⊢\neg \exists x\left(x=A\wedge x\in \varnothing \right)$$
11		dfclel	$$⊢A\in \varnothing \leftrightarrow \exists x\left(x=A\wedge x\in \varnothing \right)$$
12	10 11	mtbir	$$⊢\neg A\in \varnothing$$