Description: Obsolete version of nnz as of 1-Feb-2025. (Contributed by NM, 9-May-2004) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | nnzOLD | |- ( N e. NN -> N e. ZZ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnssz | |- NN C_ ZZ |
|
2 | 1 | sseli | |- ( N e. NN -> N e. ZZ ) |