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 0 N 0

Proof

Step Hyp Ref Expression
1 nn0uz 0 = 0
2 1 eleq2i N 0 N 0