Metamath Proof Explorer

Theorem elnn0uz

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

Ref Expression
Assertion elnn0uz 
|- ( N e. NN0 <-> N e. ( ZZ>= ` 0 ) )

Proof

Step Hyp Ref Expression
1 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
2 1 eleq2i 
 |-  ( N e. NN0 <-> N e. ( ZZ>= ` 0 ) )