Metamath Proof Explorer


Theorem elz

Description: Membership in the set of integers. (Contributed by NM, 8-Jan-2002)

Ref Expression
Assertion elz N N N = 0 N N

Proof

Step Hyp Ref Expression
1 eqeq1 x = N x = 0 N = 0
2 eleq1 x = N x N
3 negeq x = N x = N
4 3 eleq1d x = N x N
5 1 2 4 3orbi123d x = N x = 0 x x N = 0 N N
6 df-z = x | x = 0 x x
7 5 6 elrab2 N N N = 0 N N