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 ) )