Theorem nnnn0 9250

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

Assertion

Ref	Expression
nnnn0	⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℕ0)

Proof of Theorem nnnn0

Step	Hyp	Ref	Expression
1		nnssnn0 9246	. 2 ⊢ ℕ ⊆ ℕ0
2	1	sseli 3176	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2164  ℕcn 8984  ℕ₀cn0 9243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3158  df-in 3160  df-ss 3167  df-n0 9244

This theorem is referenced by:  nnnn0i  9251  elnnnn0b  9287  elnnnn0c  9288  elnn0z  9333  elz2  9391  nn0ind-raph  9437  zindd  9438  fzo1fzo0n0  10253  ubmelfzo  10270  elfzom1elp1fzo  10272  fzo0sn0fzo1  10291  modqmulnn  10416  expnegap0  10621  expcllem  10624  expcl2lemap  10625  expap0  10643  expeq0  10644  mulexpzap  10653  expnlbnd  10738  apexp1  10792  facdiv  10812  faclbnd  10815  faclbnd3  10817  faclbnd6  10818  resqrexlemlo  11160  absexpzap  11227  nnf1o  11522  summodclem2a  11527  fsum3  11533  arisum  11644  expcnvap0  11648  expcnv  11650  geo2sum  11660  geo2lim  11662  geoisum1c  11666  0.999...  11667  mertenslem2  11682  fprodseq  11729  fprodfac  11761  ef0lem  11806  ege2le3  11817  efaddlem  11820  efexp  11828  dvdsmodexp  11941  nn0enne  12046  nnehalf  12048  nno  12050  nn0o  12051  divalg2  12070  ndvdssub  12074  gcddiv  12159  gcdmultiple  12160  gcdmultiplez  12161  rpmulgcd  12166  rplpwr  12167  dvdssqlem  12170  eucalgf  12196  1nprm  12255  isprm6  12288  prmdvdsexp  12289  pw2dvds  12307  oddpwdc  12315  phicl2  12355  phibndlem  12357  phiprmpw  12363  crth  12365  hashgcdlem  12379  phisum  12381  pythagtriplem10  12410  pythagtriplem6  12411  pythagtriplem7  12412  pythagtriplem12  12416  pythagtriplem14  12418  pclemub  12428  pcexp  12450  pcid  12465  pcprod  12487  pcbc  12492  prmpwdvds  12496  infpnlem1  12500  infpnlem2  12501  prmunb  12503  1arith  12508  ennnfonelemjn  12562  ghmmulg  13329  znf1o  14150  znfi  14154  znhash  14155  znidom  14156  znidomb  14157  znrrg  14159  dvexp  14890  plycolemc  14936  logbgcd1irr  15140  lgsval4a  15179  gausslemma2dlem0c  15208  gausslemma2dlem0d  15209  gausslemma2dlem6  15224  2lgslem1a1  15243  2lgslem1c  15247  2lgslem3a1  15254  2lgslem3b1  15255  2lgslem3c1  15256  2lgslem3d1  15257