Theorem nnnn0 6107

Description: A natural number is a nonnegative integer.

Hypothesis

Ref	Expression
nnnn0.1	|- N e. NN

Assertion

Ref	Expression
nnnn0	|- N e. NN0

Proof of Theorem nnnn0

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

Syntax hints:   e. wcel 958  NNcn 5296  NN0cn0 5297

This theorem is referenced by:  1nn0 6114  2nn0 6115  faclbnd4lem1 6948  bcpasc2 6967  climubi 7153  fnsmntlem 7225  fnsmnt 7226  expcnvlem2 7228  efaddlem5 7342  efaddlem6 7343  efaddlem10 7347  efaddlem12 7349  efaddlem13 7350  efaddlem15 7352  efaddlem17 7354  efaddlem18 7355  efaddlem19 7356  efaddlem20 7357  efaddlem21 7358  efaddlem22 7359  ef1tllem 7381  ef01tllem1 7383  ef01tllem2 7384  ef01tllem2OLD 7385  absef01tllem 7387  eirrlem1 7389  eirrlem2 7390  eirrlem3 7391  eirrlem4 7392  eirrlem5 7393  ef4p 7399  efi4pt 7435  resin4pt 7436  recos4pt 7437  sin01bndlem1 7467  sin01bndlem2 7468  sin01bndlem3 7469  cos01bndlem2 7470  sin01gt0 7476

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-un 2050  df-in 2051  df-ss 2053  df-n0 6100

Copyright terms: Public domain