Metamath Proof Explorer

Theorem vn0OLD

Description: Obsolete version of vn0 as of 12-Jul-2026. (Contributed by NM, 11-Sep-2008) Avoid ax-8 , df-clel . (Revised by GG, 6-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion vn0OLD ⊢ 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 ≠ ∅