Theorem nnnn0d 9054

Description: A positive integer is a nonnegative integer. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nnnn0d.1	⊢ (𝜑 → 𝐴 ∈ ℕ)

Assertion

Ref	Expression
nnnn0d	⊢ (𝜑 → 𝐴 ∈ ℕ0)

Proof of Theorem nnnn0d

Step	Hyp	Ref	Expression
1		nnssnn0 9004	. 2 ⊢ ℕ ⊆ ℕ0
2		nnnn0d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sseldi 3100	1 ⊢ (𝜑 → 𝐴 ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 1481  ℕcn 8744  ℕ₀cn0 9001

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 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-un 3080  df-in 3082  df-ss 3089  df-n0 9002

This theorem is referenced by:  nn0ge2m1nn0  9062  nnzd  9196  eluzge2nn0  9391  modsumfzodifsn  10200  addmodlteq  10202  expnnval  10327  expgt1  10362  expaddzaplem  10367  expaddzap  10368  expmulzap  10370  expnbnd  10446  facwordi  10518  faclbnd  10519  facavg  10524  bcm1k  10538  bcval5  10541  1elfz0hash  10584  resqrexlemnm  10822  resqrexlemcvg  10823  summodc  11184  zsumdc  11185  bcxmas  11290  geo2sum  11315  geo2lim  11317  geoisum1  11320  geoisum1c  11321  cvgratnnlembern  11324  cvgratnnlemsumlt  11329  cvgratnnlemfm  11330  mertenslemi1  11336  prodmodclem3  11376  prodmodclem2a  11377  zproddc  11380  fprodseq  11384  eftabs  11399  efcllemp  11401  eftlub  11433  eirraplem  11519  dvdsfac  11594  divalglemnqt  11653  divalglemeunn  11654  gcdval  11684  gcdcl  11691  dvdsgcdidd  11718  mulgcd  11740  rplpwr  11751  rppwr  11752  lcmcl  11789  lcmgcdnn  11799  nprmdvds1  11856  rpexp  11867  pw2dvdslemn  11879  sqpweven  11889  2sqpwodd  11890  nn0sqrtelqelz  11920  phiprmpw  11934  crth  11936  logbgcd1irraplemexp  13093  cvgcmp2nlemabs  13402  trilpolemlt1  13409  redcwlpolemeq1  13421