Theorem elnn0 12502

Description: Nonnegative integers expressed in terms of naturals and zero. (Contributed by Raph Levien, 10-Dec-2002.)

Assertion

Ref	Expression
elnn0	⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

Proof of Theorem elnn0

Step	Hyp	Ref	Expression
1		df-n0 12501	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2861	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 4115	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 11196	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 4633	. . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0)
6	5	orbi2i 925	. 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
7	2, 3, 6	3bitri 300	1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

Syntax hints:   ↔ wb 209   ∨ wo 860   = wceq 1567   ∈ wcel 2149   ∪ cun 3911  {csn 4591  0cc0 11096  ℕcn 12229  ℕ₀cn0 12500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-1cn 11154  ax-icn 11155  ax-addcl 11156  ax-mulcl 11158  ax-i2m1 11164

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-sn 4592  df-n0 12501

This theorem is referenced by:  0nn0  12515  nn0ge0  12525  nnnn0addcl  12530  nnm1nn0  12541  elnnnn0b  12544  nn0sub  12550  elnn0z  12600  elznn0nn  12601  elznn0  12602  elznn  12603  nn0lt10b  12654  nn0ind-raph  12692  nn0ledivnn  13127  expp1  14100  expneg  14101  expcllem  14104  znsqcld  14194  facp1  14310  faclbnd  14322  faclbnd3  14324  faclbnd4lem1  14325  faclbnd4lem3  14327  faclbnd4  14329  bcn1  14345  bcval5  14350  hashv01gt1  14377  hashnncl  14398  seqcoll2  14498  relexpsucl  15064  relexpsucr  15065  relexpcnv  15068  relexprelg  15071  relexpdmg  15075  relexprng  15079  relexpfld  15082  relexpaddg  15086  fz1f1o  15757  arisum  15910  arisum2  15911  pwdif  15918  geomulcvg  15926  fprodfac  16023  ef0lem  16128  nn0enne  16431  nn0o1gt2  16435  bezoutlem3  16595  dfgcd2  16600  mulgcd  16602  nn0rppwr  16615  nn0expgcd  16618  eucalgf  16637  eucalginv  16638  eucalglt  16639  prmdvdsexpr  16772  rpexp1i  16778  nn0gcdsq  16807  odzdvds  16851  pceq0  16927  fldivp1  16953  pockthg  16962  1arith  16983  4sqlem17  17017  4sqlem19  17019  vdwmc2  17035  vdwlem13  17049  0ram  17076  ram0  17078  ramz  17081  ramcl  17085  ressmulgnn0  19139  mulgnn0gsum  19142  mulgnn0p1  19147  mulgnn0subcl  19149  mulgneg  19154  mulgnn0z  19163  mulgnn0dir  19166  mulgnn0ass  19172  submmulg  19180  odcl  19602  mndodcongi  19609  oddvdsnn0  19610  odnncl  19611  oddvds  19613  dfod2  19630  odcl2  19631  gexcl  19646  gexdvds  19650  gexnnod  19654  sylow1lem1  19664  mulgnn0di  19891  torsubg  19920  ablfac1eu  20141  gzrngunitlem  21547  zringlpirlem3  21579  prmirredlem  21587  prmirred  21589  znf1o  21666  evlslem3  22196  dscmet  24694  dvexp2  26078  tdeglem4  26182  dgrnznn  26369  coefv0  26370  dgreq0  26387  dgrcolem2  26396  dvply1  26410  aaliou2  26466  radcnv0  26541  logfac  26728  logtayl  26787  cxpexp  26795  birthdaylem2  27079  harmonicbnd3  27134  sqf11  27265  ppiltx  27303  sqff1o  27308  lgsdir  27458  lgsabs1  27462  lgseisenlem1  27501  2sqlem7  27550  2sqblem  27557  2sqnn  27565  chebbnd1lem1  27595  nexple  33114  xrsmulgzz  33266  ressmulgnn0d  33301  fldext2rspun  34013  eulerpartlemsv2  34689  eulerpartlemv  34695  eulerpartlemb  34699  eulerpartlemf  34701  eulerpartlemgvv  34707  eulerpartlemgh  34709  fz0n  36118  bccolsum  36126  nn0prpw  36719  aks4d1p1  42728  sticksstones13  42811  negn0nposznnd  42928  dvdsexpnn0  42980  nn0addcom  43121  nn0mulcom  43125  zmulcomlem  43126  fsuppind  43209  fzsplit1nn0  43372  pell1qrgaplem  43487  monotoddzzfi  43556  jm2.22  43609  jm2.23  43610  rmydioph  43628  expdioph  43637  rp-isfinite6  44131  relexpss1d  44318  relexpmulg  44323  iunrelexpmin2  44325  relexp0a  44329  relexpxpmin  44330  relexpaddss  44331  wallispilem3  46668  etransclem24  46859  lighneallem3  48243  lighneallem4  48246  nn0o1gt2ALTV  48343  nn0oALTV  48345  ztprmneprm  49007  blennn0elnn  49237  blen1b  49248  nn0sumshdiglem1  49281