Metamath Proof Explorer

Theorem elnnne0

Description: The positive integer property expressed in terms of difference from zero. (Contributed by Stefan O'Rear, 12-Sep-2015)

Ref Expression
Assertion elnnne0 
|- ( N e. NN <-> ( N e. NN0 /\ N =/= 0 ) )

Proof

Step Hyp Ref Expression
1 dfn2 
 |-  NN = ( NN0 \ { 0 } )
2 1 eleq2i 
 |-  ( N e. NN <-> N e. ( NN0 \ { 0 } ) )
3 eldifsn 
 |-  ( N e. ( NN0 \ { 0 } ) <-> ( N e. NN0 /\ N =/= 0 ) )
4 2 3 bitri 
 |-  ( N e. NN <-> ( N e. NN0 /\ N =/= 0 ) )