Metamath Proof Explorer

Theorem niex

Description: The class of positive integers is a set. (Contributed by NM, 15-Aug-1995) (New usage is discouraged.)

Ref Expression
Assertion niex 
|- N. e. _V

Proof

Step Hyp Ref Expression
1 omex 
 |-  _om e. _V
2 df-ni 
 |-  N. = ( _om \ { (/) } )
3 difss 
 |-  ( _om \ { (/) } ) C_ _om
4 2 3 eqsstri 
 |-  N. C_ _om
5 1 4 ssexi 
 |-  N. e. _V