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) (Proof shortened by BJ, 11-Oct-2026)

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

Proof

Step	Hyp	Ref	Expression
1		fal	$$⊢\neg \perp$$
2		dfnul4	$$⊢\varnothing =\left\{y|\perp \right\}$$
3	2	eleq2i	$$⊢x\in \varnothing \leftrightarrow x\in \left\{y|\perp \right\}$$
4		df-clab	$$⊢x\in \left\{y|\perp \right\}\leftrightarrow \left[x/y\right]\perp$$
5		sbv	$$⊢\left[x/y\right]\perp \leftrightarrow \perp$$
6	3 4 5	3bitri	$$⊢x\in \varnothing \leftrightarrow \perp$$
7	1 6	mtbir	$$⊢\neg x\in \varnothing$$
8	7	nex	$$⊢\neg \exists xx\in \varnothing$$
9		elex2	$$⊢A\in \varnothing \to \exists xx\in \varnothing$$
10	8 9	mto	$$⊢\neg A\in \varnothing$$