Metamath Proof Explorer

Theorem elnnuz

Description: A positive integer expressed as a member of an upper set of integers. (Contributed by NM, 6-Jun-2006)

Ref Expression
Assertion elnnuz 
|- ( N e. NN <-> N e. ( ZZ>= ` 1 ) )

Proof

Step Hyp Ref Expression
1 nnuz 
 |-  NN = ( ZZ>= ` 1 )
2 1 eleq2i 
 |-  ( N e. NN <-> N e. ( ZZ>= ` 1 ) )