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 fal ⊢ ¬ ⊥
2 pm5.501 ⊢ ⊤ → ⊥ ↔ ⊤ ↔ ⊥
3 2 mptru ⊢ ⊥ ↔ ⊤ ↔ ⊥
4 1 3 mtbi ⊢ ¬ ⊤ ↔ ⊥
5 4 exgen ⊢ ∃ y ¬ ⊤ ↔ ⊥
6 exnal ⊢ ∃ y ¬ ⊤ ↔ ⊥ ↔ ¬ ∀ y ⊤ ↔ ⊥
7 5 6 mpbi ⊢ ¬ ∀ y ⊤ ↔ ⊥
8 df-clab ⊢ y ∈ x | ⊤ ↔ y x ⊤
9 sbv ⊢ y x ⊤ ↔ ⊤
10 8 9 bitr2i ⊢ ⊤ ↔ y ∈ x | ⊤
11 df-clab ⊢ y ∈ x | ⊥ ↔ y x ⊥
12 sbv ⊢ y x ⊥ ↔ ⊥
13 11 12 bitr2i ⊢ ⊥ ↔ y ∈ x | ⊥
14 10 13 bibi12i ⊢ ⊤ ↔ ⊥ ↔ y ∈ x | ⊤ ↔ y ∈ x | ⊥
15 14 albii ⊢ ∀ y ⊤ ↔ ⊥ ↔ ∀ y y ∈ x | ⊤ ↔ y ∈ x | ⊥
16 7 15 mtbi ⊢ ¬ ∀ y y ∈ x | ⊤ ↔ y ∈ x | ⊥
17 dfcleq ⊢ x | ⊤ = x | ⊥ ↔ ∀ y y ∈ x | ⊤ ↔ y ∈ x | ⊥
18 dfv2 ⊢ V = x | ⊤
19 18 eqcomi ⊢ x | ⊤ = V
20 dfnul4 ⊢ ∅ = x | ⊥
21 20 eqcomi ⊢ x | ⊥ = ∅
22 19 21 eqeq12i ⊢ x | ⊤ = x | ⊥ ↔ V = ∅
23 17 22 bitr3i ⊢ ∀ y y ∈ x | ⊤ ↔ y ∈ x | ⊥ ↔ V = ∅
24 16 23 mtbi ⊢ ¬ V = ∅
25 24 neir ⊢ V ≠ ∅