Theorem nnnn0i 9147

Description: A positive integer is a nonnegative integer. (Contributed by NM, 20-Jun-2005.)

Hypothesis

Ref	Expression
nnnn0.1	|- N e. NN

Assertion

Ref	Expression
nnnn0i	|- N e. NN0

Proof of Theorem nnnn0i

Step	Hyp	Ref	Expression
1		nnnn0.1	. 2 |- N e. NN
2		nnnn0 9146	. 2 |- ( N e. NN -> N e. NN0 )
3	1, 2	ax-mp 5	1 |- N e. NN0

Syntax hints:   e. wcel 2142   NNcn 8882   NN0cn0 9139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-ext 2153

This theorem depends on definitions:  df-bi 116  df-tru 1352  df-nf 1455  df-sb 1757  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-v 2733  df-un 3126  df-in 3128  df-ss 3135  df-n0 9140

This theorem is referenced by:  1nn0  9155  2nn0  9156  3nn0  9157  4nn0  9158  5nn0  9159  6nn0  9160  7nn0  9161  8nn0  9162  9nn0  9163  numlt  9371  declei  9382  numlti  9383  pockthi  12314