Metamath Proof Explorer

Theorem nnzrab

Description: Positive integers expressed as a subset of integers. (Contributed by NM, 3-Oct-2004)

Ref Expression
Assertion nnzrab 
|- NN = { x e. ZZ | 1 <_ x }

Proof

Step Hyp Ref Expression
1 elnnz1 
 |-  ( x e. NN <-> ( x e. ZZ /\ 1 <_ x ) )
2 1 abbi2i 
 |-  NN = { x | ( x e. ZZ /\ 1 <_ x ) }
3 df-rab 
 |-  { x e. ZZ | 1 <_ x } = { x | ( x e. ZZ /\ 1 <_ x ) }
4 2 3 eqtr4i 
 |-  NN = { x e. ZZ | 1 <_ x }