Metamath Proof Explorer

Theorem nn0zrab

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

Ref Expression
Assertion nn0zrab 
|- NN0 = { x e. ZZ | 0 <_ x }

Proof

Step Hyp Ref Expression
1 elnn0z 
 |-  ( x e. NN0 <-> ( x e. ZZ /\ 0 <_ x ) )
2 1 eqabi 
 |-  NN0 = { x | ( x e. ZZ /\ 0 <_ x ) }
3 df-rab 
 |-  { x e. ZZ | 0 <_ x } = { x | ( x e. ZZ /\ 0 <_ x ) }
4 2 3 eqtr4i 
 |-  NN0 = { x e. ZZ | 0 <_ x }