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 )