Theorem noelOLD

Description: Obsolete version of noel as of 11-Oct-2026. (Contributed by NM, 21-Jun-1993) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	noelOLD	$$⊢\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$$