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

	Ref	Expression
Assertion	vn0	⊢ V ≠ ∅

Proof

Step	Hyp	Ref	Expression
1		fal	⊢ ¬ ⊥
2		vextru	⊢ 𝑦 ∈ { 𝑥 ∣ ⊤ }
3		biimp	⊢ ( ( 𝑦 ∈ { 𝑥 ∣ ⊤ } ↔ ⊥ ) → ( 𝑦 ∈ { 𝑥 ∣ ⊤ } → ⊥ ) )
4	2 3	mpi	⊢ ( ( 𝑦 ∈ { 𝑥 ∣ ⊤ } ↔ ⊥ ) → ⊥ )
5	4	spsv	⊢ ( ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ ⊤ } ↔ ⊥ ) → ⊥ )
6	1 5	mto	⊢ ¬ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ ⊤ } ↔ ⊥ )
7		dfv2	⊢ V = { 𝑥 ∣ ⊤ }
8		dfnul4	⊢ ∅ = { 𝑥 ∣ ⊥ }
9	7 8	eqeq12i	⊢ ( V = ∅ ↔ { 𝑥 ∣ ⊤ } = { 𝑥 ∣ ⊥ } )
10		biidd	⊢ ( 𝑥 = 𝑦 → ( ⊥ ↔ ⊥ ) )
11	10	eqabbw	⊢ ( { 𝑥 ∣ ⊤ } = { 𝑥 ∣ ⊥ } ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ ⊤ } ↔ ⊥ ) )
12	9 11	bitri	⊢ ( V = ∅ ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ ⊤ } ↔ ⊥ ) )
13	6 12	mtbir	⊢ ¬ V = ∅
14	13	neir	⊢ V ≠ ∅