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		fal	⊢ ¬ ⊥
2		pm5.501	⊢ ( ⊤ → ( ⊥ ↔ ( ⊤ ↔ ⊥ ) ) )
3	2	mptru	⊢ ( ⊥ ↔ ( ⊤ ↔ ⊥ ) )
4	1 3	mtbi	⊢ ¬ ( ⊤ ↔ ⊥ )
5	4	exgen	⊢ ∃ 𝑦 ¬ ( ⊤ ↔ ⊥ )
6		exnal	⊢ ( ∃ 𝑦 ¬ ( ⊤ ↔ ⊥ ) ↔ ¬ ∀ 𝑦 ( ⊤ ↔ ⊥ ) )
7	5 6	mpbi	⊢ ¬ ∀ 𝑦 ( ⊤ ↔ ⊥ )
8		df-clab	⊢ ( 𝑦 ∈ { 𝑥 ∣ ⊤ } ↔ [ 𝑦 / 𝑥 ] ⊤ )
9		sbv	⊢ ( [ 𝑦 / 𝑥 ] ⊤ ↔ ⊤ )
10	8 9	bitr2i	⊢ ( ⊤ ↔ 𝑦 ∈ { 𝑥 ∣ ⊤ } )
11		df-clab	⊢ ( 𝑦 ∈ { 𝑥 ∣ ⊥ } ↔ [ 𝑦 / 𝑥 ] ⊥ )
12		sbv	⊢ ( [ 𝑦 / 𝑥 ] ⊥ ↔ ⊥ )
13	11 12	bitr2i	⊢ ( ⊥ ↔ 𝑦 ∈ { 𝑥 ∣ ⊥ } )
14	10 13	bibi12i	⊢ ( ( ⊤ ↔ ⊥ ) ↔ ( 𝑦 ∈ { 𝑥 ∣ ⊤ } ↔ 𝑦 ∈ { 𝑥 ∣ ⊥ } ) )
15	14	albii	⊢ ( ∀ 𝑦 ( ⊤ ↔ ⊥ ) ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ ⊤ } ↔ 𝑦 ∈ { 𝑥 ∣ ⊥ } ) )
16	7 15	mtbi	⊢ ¬ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ ⊤ } ↔ 𝑦 ∈ { 𝑥 ∣ ⊥ } )
17		dfcleq	⊢ ( { 𝑥 ∣ ⊤ } = { 𝑥 ∣ ⊥ } ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ ⊤ } ↔ 𝑦 ∈ { 𝑥 ∣ ⊥ } ) )
18		dfv2	⊢ V = { 𝑥 ∣ ⊤ }
19	18	eqcomi	⊢ { 𝑥 ∣ ⊤ } = V
20		dfnul4	⊢ ∅ = { 𝑥 ∣ ⊥ }
21	20	eqcomi	⊢ { 𝑥 ∣ ⊥ } = ∅
22	19 21	eqeq12i	⊢ ( { 𝑥 ∣ ⊤ } = { 𝑥 ∣ ⊥ } ↔ V = ∅ )
23	17 22	bitr3i	⊢ ( ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ ⊤ } ↔ 𝑦 ∈ { 𝑥 ∣ ⊥ } ) ↔ V = ∅ )
24	16 23	mtbi	⊢ ¬ V = ∅
25	24	neir	⊢ V ≠ ∅