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	|- -. F.
2		pm5.501	|- ( T. -> ( F. <-> ( T. <-> F. ) ) )
3	2	mptru	|- ( F. <-> ( T. <-> F. ) )
4	1 3	mtbi	|- -. ( T. <-> F. )
5	4	exgen	|- E. y -. ( T. <-> F. )
6		exnal	|- ( E. y -. ( T. <-> F. ) <-> -. A. y ( T. <-> F. ) )
7	5 6	mpbi	|- -. A. y ( T. <-> F. )
8		df-clab	|- ( y e. { x | T. } <-> [ y / x ] T. )
9		sbv	|- ( [ y / x ] T. <-> T. )
10	8 9	bitr2i	|- ( T. <-> y e. { x | T. } )
11		df-clab	|- ( y e. { x | F. } <-> [ y / x ] F. )
12		sbv	|- ( [ y / x ] F. <-> F. )
13	11 12	bitr2i	|- ( F. <-> y e. { x | F. } )
14	10 13	bibi12i	|- ( ( T. <-> F. ) <-> ( y e. { x | T. } <-> y e. { x | F. } ) )
15	14	albii	|- ( A. y ( T. <-> F. ) <-> A. y ( y e. { x | T. } <-> y e. { x | F. } ) )
16	7 15	mtbi	|- -. A. y ( y e. { x | T. } <-> y e. { x | F. } )
17		dfcleq	|- ( { x | T. } = { x | F. } <-> A. y ( y e. { x | T. } <-> y e. { x | F. } ) )
18		dfv2	|- _V = { x | T. }
19	18	eqcomi	|- { x | T. } = _V
20		dfnul4	|- (/) = { x | F. }
21	20	eqcomi	|- { x | F. } = (/)
22	19 21	eqeq12i	|- ( { x | T. } = { x | F. } <-> _V = (/) )
23	17 22	bitr3i	|- ( A. y ( y e. { x | T. } <-> y e. { x | F. } ) <-> _V = (/) )
24	16 23	mtbi	|- -. _V = (/)
25	24	neir	|- _V =/= (/)