Theorem elnn0 12415

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 12414	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2829	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 4107	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 11138	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 4624	. . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0)
6	5	orbi2i 913	. 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
7	2, 3, 6	3bitri 297	1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

Syntax hints:   ↔ wb 206   ∨ wo 848   = wceq 1542   ∈ wcel 2114   ∪ cun 3901  {csn 4582  0cc0 11038  ℕcn 12157  ℕ₀cn0 12413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-mulcl 11100  ax-i2m1 11106

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-sn 4583  df-n0 12414

This theorem is referenced by:  0nn0  12428  nn0ge0  12438  nnnn0addcl  12443  nnm1nn0  12454  elnnnn0b  12457  nn0sub  12463  elnn0z  12513  elznn0nn  12514  elznn0  12515  elznn  12516  nn0lt10b  12566  nn0ind-raph  12604  nn0ledivnn  13032  expp1  14003  expneg  14004  expcllem  14007  znsqcld  14097  facp1  14213  faclbnd  14225  faclbnd3  14227  faclbnd4lem1  14228  faclbnd4lem3  14230  faclbnd4  14232  bcn1  14248  bcval5  14253  hashv01gt1  14280  hashnncl  14301  seqcoll2  14400  relexpsucl  14966  relexpsucr  14967  relexpcnv  14970  relexprelg  14973  relexpdmg  14977  relexprng  14981  relexpfld  14984  relexpaddg  14988  fz1f1o  15645  arisum  15795  arisum2  15796  pwdif  15803  geomulcvg  15811  fprodfac  15908  ef0lem  16013  nn0enne  16316  nn0o1gt2  16320  bezoutlem3  16480  dfgcd2  16485  mulgcd  16487  nn0rppwr  16500  nn0expgcd  16503  eucalgf  16522  eucalginv  16523  eucalglt  16524  prmdvdsexpr  16656  rpexp1i  16662  nn0gcdsq  16691  odzdvds  16735  pceq0  16811  fldivp1  16837  pockthg  16846  1arith  16867  4sqlem17  16901  4sqlem19  16903  vdwmc2  16919  vdwlem13  16933  0ram  16960  ram0  16962  ramz  16965  ramcl  16969  ressmulgnn0  19019  mulgnn0gsum  19022  mulgnn0p1  19027  mulgnn0subcl  19029  mulgneg  19034  mulgnn0z  19043  mulgnn0dir  19046  mulgnn0ass  19052  submmulg  19060  odcl  19477  mndodcongi  19484  oddvdsnn0  19485  odnncl  19486  oddvds  19488  dfod2  19505  odcl2  19506  gexcl  19521  gexdvds  19525  gexnnod  19529  sylow1lem1  19539  mulgnn0di  19766  torsubg  19795  ablfac1eu  20016  gzrngunitlem  21399  zringlpirlem3  21431  prmirredlem  21439  prmirred  21441  znf1o  21518  evlslem3  22047  dscmet  24528  dvexp2  25926  tdeglem4  26033  dgrnznn  26220  coefv0  26221  dgreq0  26239  dgrcolem2  26248  dvply1  26259  aaliou2  26316  radcnv0  26393  logfac  26578  logtayl  26637  cxpexp  26645  birthdaylem2  26930  harmonicbnd3  26986  sqf11  27117  ppiltx  27155  sqff1o  27160  lgsdir  27311  lgsabs1  27315  lgseisenlem1  27354  2sqlem7  27403  2sqblem  27410  2sqnn  27418  chebbnd1lem1  27448  nexple  32936  xrsmulgzz  33102  ressmulgnn0d  33138  fldext2rspun  33860  eulerpartlemsv2  34536  eulerpartlemv  34542  eulerpartlemb  34546  eulerpartlemf  34548  eulerpartlemgvv  34554  eulerpartlemgh  34556  fz0n  35947  bccolsum  35955  nn0prpw  36539  aks4d1p1  42446  sticksstones13  42529  negn0nposznnd  42652  dvdsexpnn0  42704  nn0addcom  42832  nn0mulcom  42836  zmulcomlem  42837  fsuppind  42948  fzsplit1nn0  43111  pell1qrgaplem  43230  monotoddzzfi  43299  jm2.22  43352  jm2.23  43353  rmydioph  43371  expdioph  43380  rp-isfinite6  43874  relexpss1d  44061  relexpmulg  44066  iunrelexpmin2  44068  relexp0a  44072  relexpxpmin  44073  relexpaddss  44074  wallispilem3  46425  etransclem24  46616  lighneallem3  47967  lighneallem4  47970  nn0o1gt2ALTV  48054  nn0oALTV  48056  ztprmneprm  48707  blennn0elnn  48937  blen1b  48948  nn0sumshdiglem1  48981