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 ≠ ∅