Theorem elnn0 12403

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 12402	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2828	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 4105	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 11126	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 4622	. . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0)
6	5	orbi2i 912	. 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
7	2, 3, 6	3bitri 297	1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

Syntax hints:   ↔ wb 206   ∨ wo 847   = wceq 1541   ∈ wcel 2113   ∪ cun 3899  {csn 4580  0cc0 11026  ℕcn 12145  ℕ₀cn0 12401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-mulcl 11088  ax-i2m1 11094

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-sn 4581  df-n0 12402

This theorem is referenced by:  0nn0  12416  nn0ge0  12426  nnnn0addcl  12431  nnm1nn0  12442  elnnnn0b  12445  nn0sub  12451  elnn0z  12501  elznn0nn  12502  elznn0  12503  elznn  12504  nn0lt10b  12554  nn0ind-raph  12592  nn0ledivnn  13020  expp1  13991  expneg  13992  expcllem  13995  znsqcld  14085  facp1  14201  faclbnd  14213  faclbnd3  14215  faclbnd4lem1  14216  faclbnd4lem3  14218  faclbnd4  14220  bcn1  14236  bcval5  14241  hashv01gt1  14268  hashnncl  14289  seqcoll2  14388  relexpsucl  14954  relexpsucr  14955  relexpcnv  14958  relexprelg  14961  relexpdmg  14965  relexprng  14969  relexpfld  14972  relexpaddg  14976  fz1f1o  15633  arisum  15783  arisum2  15784  pwdif  15791  geomulcvg  15799  fprodfac  15896  ef0lem  16001  nn0enne  16304  nn0o1gt2  16308  bezoutlem3  16468  dfgcd2  16473  mulgcd  16475  nn0rppwr  16488  nn0expgcd  16491  eucalgf  16510  eucalginv  16511  eucalglt  16512  prmdvdsexpr  16644  rpexp1i  16650  nn0gcdsq  16679  odzdvds  16723  pceq0  16799  fldivp1  16825  pockthg  16834  1arith  16855  4sqlem17  16889  4sqlem19  16891  vdwmc2  16907  vdwlem13  16921  0ram  16948  ram0  16950  ramz  16953  ramcl  16957  ressmulgnn0  19007  mulgnn0gsum  19010  mulgnn0p1  19015  mulgnn0subcl  19017  mulgneg  19022  mulgnn0z  19031  mulgnn0dir  19034  mulgnn0ass  19040  submmulg  19048  odcl  19465  mndodcongi  19472  oddvdsnn0  19473  odnncl  19474  oddvds  19476  dfod2  19493  odcl2  19494  gexcl  19509  gexdvds  19513  gexnnod  19517  sylow1lem1  19527  mulgnn0di  19754  torsubg  19783  ablfac1eu  20004  gzrngunitlem  21387  zringlpirlem3  21419  prmirredlem  21427  prmirred  21429  znf1o  21506  evlslem3  22035  dscmet  24516  dvexp2  25914  tdeglem4  26021  dgrnznn  26208  coefv0  26209  dgreq0  26227  dgrcolem2  26236  dvply1  26247  aaliou2  26304  radcnv0  26381  logfac  26566  logtayl  26625  cxpexp  26633  birthdaylem2  26918  harmonicbnd3  26974  sqf11  27105  ppiltx  27143  sqff1o  27148  lgsdir  27299  lgsabs1  27303  lgseisenlem1  27342  2sqlem7  27391  2sqblem  27398  2sqnn  27406  chebbnd1lem1  27436  nexple  32925  xrsmulgzz  33091  ressmulgnn0d  33127  fldext2rspun  33839  eulerpartlemsv2  34515  eulerpartlemv  34521  eulerpartlemb  34525  eulerpartlemf  34527  eulerpartlemgvv  34533  eulerpartlemgh  34535  fz0n  35925  bccolsum  35933  nn0prpw  36517  aks4d1p1  42330  sticksstones13  42413  negn0nposznnd  42537  dvdsexpnn0  42589  nn0addcom  42717  nn0mulcom  42721  zmulcomlem  42722  fsuppind  42833  fzsplit1nn0  42996  pell1qrgaplem  43115  monotoddzzfi  43184  jm2.22  43237  jm2.23  43238  rmydioph  43256  expdioph  43265  rp-isfinite6  43759  relexpss1d  43946  relexpmulg  43951  iunrelexpmin2  43953  relexp0a  43957  relexpxpmin  43958  relexpaddss  43959  wallispilem3  46311  etransclem24  46502  lighneallem3  47853  lighneallem4  47856  nn0o1gt2ALTV  47940  nn0oALTV  47942  ztprmneprm  48593  blennn0elnn  48823  blen1b  48834  nn0sumshdiglem1  48867