Metamath Proof Explorer


Theorem onnevOLD

Description: Obsolete version of onnev as of 27-May-2024. (Contributed by NM, 16-Jun-2007) (Proof shortened by Mario Carneiro, 10-Jan-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion onnevOLD
|- On =/= _V

Proof

Step Hyp Ref Expression
1 snsn0non
 |-  -. { { (/) } } e. On
2 snex
 |-  { { (/) } } e. _V
3 id
 |-  ( On = _V -> On = _V )
4 2 3 eleqtrrid
 |-  ( On = _V -> { { (/) } } e. On )
5 4 necon3bi
 |-  ( -. { { (/) } } e. On -> On =/= _V )
6 1 5 ax-mp
 |-  On =/= _V