Theorem elnn0 12420

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 12419	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2820	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 4112	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 11144	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 4625	. . 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 1540   ∈ wcel 2109   ∪ cun 3909  {csn 4585  0cc0 11044  ℕcn 12162  ℕ₀cn0 12418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-mulcl 11106  ax-i2m1 11112

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-un 3916  df-sn 4586  df-n0 12419

This theorem is referenced by:  0nn0  12433  nn0ge0  12443  nnnn0addcl  12448  nnm1nn0  12459  elnnnn0b  12462  nn0sub  12468  elnn0z  12518  elznn0nn  12519  elznn0  12520  elznn  12521  nn0lt10b  12572  nn0ind-raph  12610  nn0ledivnn  13042  expp1  14009  expneg  14010  expcllem  14013  znsqcld  14103  facp1  14219  faclbnd  14231  faclbnd3  14233  faclbnd4lem1  14234  faclbnd4lem3  14236  faclbnd4  14238  bcn1  14254  bcval5  14259  hashv01gt1  14286  hashnncl  14307  seqcoll2  14406  relexpsucl  14973  relexpsucr  14974  relexpcnv  14977  relexprelg  14980  relexpdmg  14984  relexprng  14988  relexpfld  14991  relexpaddg  14995  fz1f1o  15652  arisum  15802  arisum2  15803  pwdif  15810  geomulcvg  15818  fprodfac  15915  ef0lem  16020  nn0enne  16323  nn0o1gt2  16327  bezoutlem3  16487  dfgcd2  16492  mulgcd  16494  nn0rppwr  16507  nn0expgcd  16510  eucalgf  16529  eucalginv  16530  eucalglt  16531  prmdvdsexpr  16663  rpexp1i  16669  nn0gcdsq  16698  odzdvds  16742  pceq0  16818  fldivp1  16844  pockthg  16853  1arith  16874  4sqlem17  16908  4sqlem19  16910  vdwmc2  16926  vdwlem13  16940  0ram  16967  ram0  16969  ramz  16972  ramcl  16976  ressmulgnn0  18985  mulgnn0gsum  18988  mulgnn0p1  18993  mulgnn0subcl  18995  mulgneg  19000  mulgnn0z  19009  mulgnn0dir  19012  mulgnn0ass  19018  submmulg  19026  odcl  19442  mndodcongi  19449  oddvdsnn0  19450  odnncl  19451  oddvds  19453  dfod2  19470  odcl2  19471  gexcl  19486  gexdvds  19490  gexnnod  19494  sylow1lem1  19504  mulgnn0di  19731  torsubg  19760  ablfac1eu  19981  gzrngunitlem  21325  zringlpirlem3  21350  prmirredlem  21358  prmirred  21360  znf1o  21437  evlslem3  21963  dscmet  24436  dvexp2  25834  tdeglem4  25941  dgrnznn  26128  coefv0  26129  dgreq0  26147  dgrcolem2  26156  dvply1  26167  aaliou2  26224  radcnv0  26301  logfac  26486  logtayl  26545  cxpexp  26553  birthdaylem2  26838  harmonicbnd3  26894  sqf11  27025  ppiltx  27063  sqff1o  27068  lgsdir  27219  lgsabs1  27223  lgseisenlem1  27262  2sqlem7  27311  2sqblem  27318  2sqnn  27326  chebbnd1lem1  27356  nexple  32742  xrsmulgzz  32920  ressmulgnn0d  32958  fldext2rspun  33650  eulerpartlemsv2  34322  eulerpartlemv  34328  eulerpartlemb  34332  eulerpartlemf  34334  eulerpartlemgvv  34340  eulerpartlemgh  34342  fz0n  35691  bccolsum  35699  nn0prpw  36284  aks4d1p1  42037  sticksstones13  42120  negn0nposznnd  42243  dvdsexpnn0  42295  nn0addcom  42423  nn0mulcom  42427  zmulcomlem  42428  fsuppind  42551  fzsplit1nn0  42715  pell1qrgaplem  42834  monotoddzzfi  42904  jm2.22  42957  jm2.23  42958  rmydioph  42976  expdioph  42985  rp-isfinite6  43480  relexpss1d  43667  relexpmulg  43672  iunrelexpmin2  43674  relexp0a  43678  relexpxpmin  43679  relexpaddss  43680  wallispilem3  46038  etransclem24  46229  lighneallem3  47581  lighneallem4  47584  nn0o1gt2ALTV  47668  nn0oALTV  47670  ztprmneprm  48308  blennn0elnn  48539  blen1b  48550  nn0sumshdiglem1  48583