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