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

Ref Expression
Assertion vn0 ⊢ V ≠ ∅

Proof

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