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 = { 𝑦 ∣ ⊤ }
3		dfnul4	⊢ ∅ = { 𝑧 ∣ ⊥ }
4	2 3	eqeq12i	⊢ ( V = ∅ ↔ { 𝑦 ∣ ⊤ } = { 𝑧 ∣ ⊥ } )
5		dfcleq	⊢ ( { 𝑦 ∣ ⊤ } = { 𝑧 ∣ ⊥ } ↔ ∀ 𝑥 ( 𝑥 ∈ { 𝑦 ∣ ⊤ } ↔ 𝑥 ∈ { 𝑧 ∣ ⊥ } ) )
6		df-clab	⊢ ( 𝑥 ∈ { 𝑦 ∣ ⊤ } ↔ [ 𝑥 / 𝑦 ] ⊤ )
7		sbv	⊢ ( [ 𝑥 / 𝑦 ] ⊤ ↔ ⊤ )
8	6 7	bitri	⊢ ( 𝑥 ∈ { 𝑦 ∣ ⊤ } ↔ ⊤ )
9		df-clab	⊢ ( 𝑥 ∈ { 𝑧 ∣ ⊥ } ↔ [ 𝑥 / 𝑧 ] ⊥ )
10		sbv	⊢ ( [ 𝑥 / 𝑧 ] ⊥ ↔ ⊥ )
11	9 10	bitri	⊢ ( 𝑥 ∈ { 𝑧 ∣ ⊥ } ↔ ⊥ )
12	8 11	bibi12i	⊢ ( ( 𝑥 ∈ { 𝑦 ∣ ⊤ } ↔ 𝑥 ∈ { 𝑧 ∣ ⊥ } ) ↔ ( ⊤ ↔ ⊥ ) )
13		trubifal	⊢ ( ( ⊤ ↔ ⊥ ) ↔ ⊥ )
14	12 13	sylbb	⊢ ( ( 𝑥 ∈ { 𝑦 ∣ ⊤ } ↔ 𝑥 ∈ { 𝑧 ∣ ⊥ } ) → ⊥ )
15	14	spsv	⊢ ( ∀ 𝑥 ( 𝑥 ∈ { 𝑦 ∣ ⊤ } ↔ 𝑥 ∈ { 𝑧 ∣ ⊥ } ) → ⊥ )
16	5 15	sylbi	⊢ ( { 𝑦 ∣ ⊤ } = { 𝑧 ∣ ⊥ } → ⊥ )
17	4 16	sylbi	⊢ ( V = ∅ → ⊥ )
18	1 17	mto	⊢ ¬ V = ∅
19	18	neir	⊢ V ≠ ∅