This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 =/= (/)