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) (Proof shortened by BJ, 12-Jul-2026)

	Ref	Expression
Assertion	vn0	|- _V =/= (/)

Proof

Step	Hyp	Ref	Expression
1		fal	|- -. F.
2		vextru	|- y e. { x | T. }
3		biimp	|- ( ( y e. { x | T. } <-> F. ) -> ( y e. { x | T. } -> F. ) )
4	2 3	mpi	|- ( ( y e. { x | T. } <-> F. ) -> F. )
5	4	spsv	|- ( A. y ( y e. { x | T. } <-> F. ) -> F. )
6	1 5	mto	|- -. A. y ( y e. { x | T. } <-> F. )
7		dfv2	|- _V = { x | T. }
8		dfnul4	|- (/) = { x | F. }
9	7 8	eqeq12i	|- ( _V = (/) <-> { x | T. } = { x | F. } )
10		biidd	|- ( x = y -> ( F. <-> F. ) )
11	10	eqabbw	|- ( { x | T. } = { x | F. } <-> A. y ( y e. { x | T. } <-> F. ) )
12	9 11	bitri	|- ( _V = (/) <-> A. y ( y e. { x | T. } <-> F. ) )
13	6 12	mtbir	|- -. _V = (/)
14	13	neir	|- _V =/= (/)