Metamath Proof Explorer

Theorem bj-vn0ALT

Description: Alternate proof of vn0 which does not use eqabbw (and is shorter than vn0 when eqabbw is inlined). (Contributed by BJ, 12-Jul-2026) Using the same dummy variable for y and z slightly reduces the proof size. (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion bj-vn0ALT ⊢ V ≠ ∅

Proof

Step Hyp Ref Expression
1 fal ⊢ ¬ ⊥
2 dfv2 ⊢ V = y | ⊤
3 dfnul4 ⊢ ∅ = z | ⊥
4 2 3 eqeq12i ⊢ V = ∅ ↔ y | ⊤ = z | ⊥
5 dfcleq ⊢ y | ⊤ = z | ⊥ ↔ ∀ x x ∈ y | ⊤ ↔ x ∈ z | ⊥
6 df-clab ⊢ x ∈ y | ⊤ ↔ x y ⊤
7 sbv ⊢ x y ⊤ ↔ ⊤
8 6 7 bitri ⊢ x ∈ y | ⊤ ↔ ⊤
9 df-clab ⊢ x ∈ z | ⊥ ↔ x z ⊥
10 sbv ⊢ x z ⊥ ↔ ⊥
11 9 10 bitri ⊢ x ∈ z | ⊥ ↔ ⊥
12 8 11 bibi12i ⊢ x ∈ y | ⊤ ↔ x ∈ z | ⊥ ↔ ⊤ ↔ ⊥
13 trubifal ⊢ ⊤ ↔ ⊥ ↔ ⊥
14 12 13 sylbb ⊢ x ∈ y | ⊤ ↔ x ∈ z | ⊥ → ⊥
15 14 spsv ⊢ ∀ x x ∈ y | ⊤ ↔ x ∈ z | ⊥ → ⊥
16 5 15 sylbi ⊢ y | ⊤ = z | ⊥ → ⊥
17 4 16 sylbi ⊢ V = ∅ → ⊥
18 1 17 mto ⊢ ¬ V = ∅
19 18 neir ⊢ V ≠ ∅