Metamath Proof Explorer

Theorem vn0

Description: The universal class is not equal to the empty set. (Contributed by NM, 11-Sep-2008) Avoid ax-8 , df-clel . (Revised by GG, 6-Sep-2024)

		Ref	Expression
	Assertion	vn0	$⊢ V \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		vextru	$⊢ y \in \{x \| ⊤\}$
2		fal	$⊢ \neg ⊥$
3	1 2	2th	$⊢ y \in \{x \| ⊤\} \leftrightarrow \neg ⊥$
4		xor3	$⊢ \neg (y \in \{x \| ⊤\} \leftrightarrow ⊥) \leftrightarrow (y \in \{x \| ⊤\} \leftrightarrow \neg ⊥)$
5	3 4	mpbir	$⊢ \neg (y \in \{x \| ⊤\} \leftrightarrow ⊥)$
6	5	exgen	$⊢ \exists y \neg (y \in \{x \| ⊤\} \leftrightarrow ⊥)$
7		exnal	$⊢ \exists y \neg (y \in \{x \| ⊤\} \leftrightarrow ⊥) \leftrightarrow \neg \forall y (y \in \{x \| ⊤\} \leftrightarrow ⊥)$
8	6 7	mpbi	$⊢ \neg \forall y (y \in \{x \| ⊤\} \leftrightarrow ⊥)$
9		dfv2	$⊢ V = \{x \| ⊤\}$
10		dfnul4	$⊢ \emptyset = \{x \| ⊥\}$
11	9 10	eqeq12i	$⊢ V = \emptyset \leftrightarrow \{x \| ⊤\} = \{x \| ⊥\}$
12		biidd	$⊢ x = y \to (⊥ \leftrightarrow ⊥)$
13	12	eqabbw	$⊢ \{x \| ⊤\} = \{x \| ⊥\} \leftrightarrow \forall y (y \in \{x \| ⊤\} \leftrightarrow ⊥)$
14	11 13	bitri	$⊢ V = \emptyset \leftrightarrow \forall y (y \in \{x \| ⊤\} \leftrightarrow ⊥)$
15	8 14	mtbir	$⊢ \neg V = \emptyset$
16	15	neir	$⊢ V \neq \emptyset$