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	|- y e. { x | T. }
2		fal	|- -. F.
3	1 2	2th	|- ( y e. { x | T. } <-> -. F. )
4		xor3	|- ( -. ( y e. { x | T. } <-> F. ) <-> ( y e. { x | T. } <-> -. F. ) )
5	3 4	mpbir	|- -. ( y e. { x | T. } <-> F. )
6	5	exgen	|- E. y -. ( y e. { x | T. } <-> F. )
7		exnal	|- ( E. y -. ( y e. { x | T. } <-> F. ) <-> -. A. y ( y e. { x | T. } <-> F. ) )
8	6 7	mpbi	|- -. A. y ( y e. { x | T. } <-> F. )
9		dfv2	|- _V = { x | T. }
10		dfnul4	|- (/) = { x | F. }
11	9 10	eqeq12i	|- ( _V = (/) <-> { x | T. } = { x | F. } )
12		biidd	|- ( x = y -> ( F. <-> F. ) )
13	12	eqabbw	|- ( { x | T. } = { x | F. } <-> A. y ( y e. { x | T. } <-> F. ) )
14	11 13	bitri	|- ( _V = (/) <-> A. y ( y e. { x | T. } <-> F. ) )
15	8 14	mtbir	|- -. _V = (/)
16	15	neir	|- _V =/= (/)