Metamath Proof Explorer

Theorem 0npi

Description: The empty set is not a positive integer. (Contributed by NM, 26-Aug-1995) (New usage is discouraged.)

Ref Expression
Assertion 0npi 
|- -. (/) e. N.

Proof

Step Hyp Ref Expression
1 eqid 
 |-  (/) = (/)
2 elni 
 |-  ( (/) e. N. <-> ( (/) e. _om /\ (/) =/= (/) ) )
3 2 simprbi 
 |-  ( (/) e. N. -> (/) =/= (/) )
4 3 necon2bi 
 |-  ( (/) = (/) -> -. (/) e. N. )
5 1 4 ax-mp 
 |-  -. (/) e. N.