Metamath Proof Explorer

Theorem noelOLD

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

		Ref	Expression
	Assertion	noelOLD	$⊢ \neg A \in \emptyset$

Proof

Step	Hyp	Ref	Expression
1		pm3.24	$⊢ \neg (y \in V \land \neg y \in V)$
2	1	nex	$⊢ \neg \exists y (y \in V \land \neg y \in V)$
3		df-clab	$⊢ x \in \{y \| (y \in V \land \neg y \in V)\} \leftrightarrow [x/ y] (y \in V \land \neg y \in V)$
4		spsbe	$⊢ [x/ y] (y \in V \land \neg y \in V) \to \exists y (y \in V \land \neg y \in V)$
5	3 4	sylbi	$⊢ x \in \{y \| (y \in V \land \neg y \in V)\} \to \exists y (y \in V \land \neg y \in V)$
6	2 5	mto	$⊢ \neg x \in \{y \| (y \in V \land \neg y \in V)\}$
7		df-nul	$⊢ \emptyset = V ∖ V$
8		df-dif	$⊢ V ∖ V = \{y \| (y \in V \land \neg y \in V)\}$
9	7 8	eqtri	$⊢ \emptyset = \{y \| (y \in V \land \neg y \in V)\}$
10	9	eleq2i	$⊢ x \in \emptyset \leftrightarrow x \in \{y \| (y \in V \land \neg y \in V)\}$
11	6 10	mtbir	$⊢ \neg x \in \emptyset$
12	11	intnan	$⊢ \neg (x = A \land x \in \emptyset)$
13	12	nex	$⊢ \neg \exists x (x = A \land x \in \emptyset)$
14		dfclel	$⊢ A \in \emptyset \leftrightarrow \exists x (x = A \land x \in \emptyset)$
15	13 14	mtbir	$⊢ \neg A \in \emptyset$