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 Gino Giotto, 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|⊤↔yx⊤
9 sbv ⊢yx⊤↔⊤
10 8 9 bitr2i ⊢⊤↔y∈x|⊤
11 df-clab ⊢y∈x|⊥↔yx⊥
12 sbv ⊢yx⊥↔⊥
13 11 12 bitr2i ⊢⊥↔y∈x|⊥
14 10 13 bibi12i ⊢⊤↔⊥↔y∈x|⊤↔y∈x|⊥
15 14 albii ⊢∀y⊤↔⊥↔∀yy∈x|⊤↔y∈x|⊥
16 7 15 mtbi ⊢¬∀yy∈x|⊤↔y∈x|⊥
17 dfcleq ⊢x|⊤=x|⊥↔∀yy∈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 ⊢∀yy∈x|⊤↔y∈x|⊥↔V=∅
24 16 23 mtbi ⊢¬V=∅
25 24 neir ⊢V≠∅