Metamath Proof Explorer
Description: The empty set is not a positive integer. (Contributed by NM, 26Aug1995) (New usage is discouraged.)


Ref 
Expression 

Assertion 
0npi 
⊢ ¬ ∅ ∈ N 
Proof
Step 
Hyp 
Ref 
Expression 
1 

eqid 
⊢ ∅ = ∅ 
2 

elni 
⊢ ( ∅ ∈ N ↔ ( ∅ ∈ ω ∧ ∅ ≠ ∅ ) ) 
3 
2

simprbi 
⊢ ( ∅ ∈ N → ∅ ≠ ∅ ) 
4 
3

necon2bi 
⊢ ( ∅ = ∅ → ¬ ∅ ∈ N ) 
5 
1 4

axmp 
⊢ ¬ ∅ ∈ N 