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 ⊢ 𝑦 ∈ { 𝑥 ∣ ⊤ }
2 fal ⊢ ¬ ⊥
3 1 2 2th ⊢ ( 𝑦 ∈ { 𝑥 ∣ ⊤ } ↔ ¬ ⊥ )
4 xor3 ⊢ ( ¬ ( 𝑦 ∈ { 𝑥 ∣ ⊤ } ↔ ⊥ ) ↔ ( 𝑦 ∈ { 𝑥 ∣ ⊤ } ↔ ¬ ⊥ ) )
5 3 4 mpbir ⊢ ¬ ( 𝑦 ∈ { 𝑥 ∣ ⊤ } ↔ ⊥ )
6 5 exgen ⊢ ∃ 𝑦 ¬ ( 𝑦 ∈ { 𝑥 ∣ ⊤ } ↔ ⊥ )
7 exnal ⊢ ( ∃ 𝑦 ¬ ( 𝑦 ∈ { 𝑥 ∣ ⊤ } ↔ ⊥ ) ↔ ¬ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ ⊤ } ↔ ⊥ ) )
8 6 7 mpbi ⊢ ¬ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ ⊤ } ↔ ⊥ )
9 dfv2 ⊢ V = { 𝑥 ∣ ⊤ }
10 dfnul4 ⊢ ∅ = { 𝑥 ∣ ⊥ }
11 9 10 eqeq12i ⊢ ( V = ∅ ↔ { 𝑥 ∣ ⊤ } = { 𝑥 ∣ ⊥ } )
12 biidd ⊢ ( 𝑥 = 𝑦 → ( ⊥ ↔ ⊥ ) )
13 12 eqabbw ⊢ ( { 𝑥 ∣ ⊤ } = { 𝑥 ∣ ⊥ } ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ ⊤ } ↔ ⊥ ) )
14 11 13 bitri ⊢ ( V = ∅ ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ ⊤ } ↔ ⊥ ) )
15 8 14 mtbir ⊢ ¬ V = ∅
16 15 neir ⊢ V ≠ ∅