This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ≠ ∅

Proof

Step Hyp Ref Expression
1 vextru ⊢ y ∈ x | ⊤
2 fal ⊢ ¬ ⊥
3 1 2 2th ⊢ y ∈ x | ⊤ ↔ ¬ ⊥
4 xor3 ⊢ ¬ y ∈ x | ⊤ ↔ ⊥ ↔ y ∈ x | ⊤ ↔ ¬ ⊥
5 3 4 mpbir ⊢ ¬ y ∈ x | ⊤ ↔ ⊥
6 5 exgen ⊢ ∃ y ¬ y ∈ x | ⊤ ↔ ⊥
7 exnal ⊢ ∃ y ¬ y ∈ x | ⊤ ↔ ⊥ ↔ ¬ ∀ y y ∈ x | ⊤ ↔ ⊥
8 6 7 mpbi ⊢ ¬ ∀ y y ∈ x | ⊤ ↔ ⊥
9 dfv2 ⊢ V = x | ⊤
10 dfnul4 ⊢ ∅ = x | ⊥
11 9 10 eqeq12i ⊢ V = ∅ ↔ x | ⊤ = x | ⊥
12 biidd ⊢ x = y → ⊥ ↔ ⊥
13 12 eqabbw ⊢ x | ⊤ = x | ⊥ ↔ ∀ y y ∈ x | ⊤ ↔ ⊥
14 11 13 bitri ⊢ V = ∅ ↔ ∀ y y ∈ x | ⊤ ↔ ⊥
15 8 14 mtbir ⊢ ¬ V = ∅
16 15 neir ⊢ V ≠ ∅