Metamath Proof Explorer

Theorem elni

Description: Membership in the class of positive integers. (Contributed by NM, 15-Aug-1995) (New usage is discouraged.)

Ref Expression
Assertion elni 
|- ( A e. N. <-> ( A e. _om /\ A =/= (/) ) )

Proof

Step Hyp Ref Expression
1 df-ni 
 |-  N. = ( _om \ { (/) } )
2 1 eleq2i 
 |-  ( A e. N. <-> A e. ( _om \ { (/) } ) )
3 eldifsn 
 |-  ( A e. ( _om \ { (/) } ) <-> ( A e. _om /\ A =/= (/) ) )
4 2 3 bitri 
 |-  ( A e. N. <-> ( A e. _om /\ A =/= (/) ) )