Metamath Proof Explorer

Theorem elni2

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

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

Proof

Step Hyp Ref Expression
1 elni 
 |-  ( A e. N. <-> ( A e. _om /\ A =/= (/) ) )
2 nnord 
 |-  ( A e. _om -> Ord A )
3 ord0eln0 
 |-  ( Ord A -> ( (/) e. A <-> A =/= (/) ) )
4 2 3 syl 
 |-  ( A e. _om -> ( (/) e. A <-> A =/= (/) ) )
5 4 pm5.32i 
 |-  ( ( A e. _om /\ (/) e. A ) <-> ( A e. _om /\ A =/= (/) ) )
6 1 5 bitr4i 
 |-  ( A e. N. <-> ( A e. _om /\ (/) e. A ) )