Theorem nnnn0 8188

Description: A positive integer is a nonnegative integer. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
nnnn0	|- ( A e. NN -> A e. NN0 )

Proof of Theorem nnnn0

Step	Hyp	Ref	Expression
1		nnssnn0 8184	. 2 |- NN C_ NN0
2	1	sseli 2941	1 |- ( A e. NN -> A e. NN0 )

Syntax hints:   -> wi 4   e. wcel 1393   NNcn 7914   NN0cn0 8181

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-v 2559  df-un 2922  df-in 2924  df-ss 2931  df-n0 8182

This theorem is referenced by:  nnnn0i  8189  elnnnn0b  8226  elnnnn0c  8227  elnn0z  8258  elz2  8312  nn0ind-raph  8355  zindd  8356  fzo1fzo0n0  9039  ubmelfzo  9056  elfzom1elp1fzo  9058  fzo0sn0fzo1  9077  modqmulnn  9184  expnegap0  9263  expcllem  9266  expcl2lemap  9267  expap0  9285  expeq0  9286  mulexpzap  9295  expnlbnd  9373  resqrexlemlo  9611  absexpzap  9676