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 \emptyset$

Proof

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

Metamath Proof Explorer

Theorem noel

Proof