Description: The set of positive integers exists. (Contributed by NM, 3Oct1999) (Revised by Mario Carneiro, 17Nov2014)
Ref  Expression  

Assertion  nnex   NN e. _V 
Step  Hyp  Ref  Expression 

1  cnex   CC e. _V 

2  nnsscn   NN C_ CC 

3  1 2  ssexi   NN e. _V 