Metamath Proof Explorer


Theorem pinn

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 )

Proof

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 )