Description: A positive integer is a natural number. (Contributed by NM, 15-Aug-1995) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | pinn | |- ( A e. N. -> A e. _om ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ni | |- N. = ( _om \ { (/) } ) |
|
2 | difss | |- ( _om \ { (/) } ) C_ _om |
|
3 | 1 2 | eqsstri | |- N. C_ _om |
4 | 3 | sseli | |- ( A e. N. -> A e. _om ) |