Theorem elnn0 12439

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 12438	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2828	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 4093	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 11138	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 4609	. . 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 3887  {csn 4567  0cc0 11038  ℕcn 12174  ℕ₀cn0 12437

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 2708  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 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-sn 4568  df-n0 12438

This theorem is referenced by:  0nn0  12452  nn0ge0  12462  nnnn0addcl  12467  nnm1nn0  12478  elnnnn0b  12481  nn0sub  12487  elnn0z  12537  elznn0nn  12538  elznn0  12539  elznn  12540  nn0lt10b  12591  nn0ind-raph  12629  nn0ledivnn  13057  expp1  14030  expneg  14031  expcllem  14034  znsqcld  14124  facp1  14240  faclbnd  14252  faclbnd3  14254  faclbnd4lem1  14255  faclbnd4lem3  14257  faclbnd4  14259  bcn1  14275  bcval5  14280  hashv01gt1  14307  hashnncl  14328  seqcoll2  14427  relexpsucl  14993  relexpsucr  14994  relexpcnv  14997  relexprelg  15000  relexpdmg  15004  relexprng  15008  relexpfld  15011  relexpaddg  15015  fz1f1o  15672  arisum  15825  arisum2  15826  pwdif  15833  geomulcvg  15841  fprodfac  15938  ef0lem  16043  nn0enne  16346  nn0o1gt2  16350  bezoutlem3  16510  dfgcd2  16515  mulgcd  16517  nn0rppwr  16530  nn0expgcd  16533  eucalgf  16552  eucalginv  16553  eucalglt  16554  prmdvdsexpr  16687  rpexp1i  16693  nn0gcdsq  16722  odzdvds  16766  pceq0  16842  fldivp1  16868  pockthg  16877  1arith  16898  4sqlem17  16932  4sqlem19  16934  vdwmc2  16950  vdwlem13  16964  0ram  16991  ram0  16993  ramz  16996  ramcl  17000  ressmulgnn0  19053  mulgnn0gsum  19056  mulgnn0p1  19061  mulgnn0subcl  19063  mulgneg  19068  mulgnn0z  19077  mulgnn0dir  19080  mulgnn0ass  19086  submmulg  19094  odcl  19511  mndodcongi  19518  oddvdsnn0  19519  odnncl  19520  oddvds  19522  dfod2  19539  odcl2  19540  gexcl  19555  gexdvds  19559  gexnnod  19563  sylow1lem1  19573  mulgnn0di  19800  torsubg  19829  ablfac1eu  20050  gzrngunitlem  21412  zringlpirlem3  21444  prmirredlem  21452  prmirred  21454  znf1o  21531  evlslem3  22058  dscmet  24537  dvexp2  25921  tdeglem4  26025  dgrnznn  26212  coefv0  26213  dgreq0  26230  dgrcolem2  26239  dvply1  26250  aaliou2  26306  radcnv0  26381  logfac  26565  logtayl  26624  cxpexp  26632  birthdaylem2  26916  harmonicbnd3  26971  sqf11  27102  ppiltx  27140  sqff1o  27145  lgsdir  27295  lgsabs1  27299  lgseisenlem1  27338  2sqlem7  27387  2sqblem  27394  2sqnn  27402  chebbnd1lem1  27432  nexple  32917  xrsmulgzz  33069  ressmulgnn0d  33105  fldext2rspun  33826  eulerpartlemsv2  34502  eulerpartlemv  34508  eulerpartlemb  34512  eulerpartlemf  34514  eulerpartlemgvv  34520  eulerpartlemgh  34522  fz0n  35913  bccolsum  35921  nn0prpw  36505  aks4d1p1  42515  sticksstones13  42598  negn0nposznnd  42714  dvdsexpnn0  42766  nn0addcom  42907  nn0mulcom  42911  zmulcomlem  42912  fsuppind  43023  fzsplit1nn0  43186  pell1qrgaplem  43301  monotoddzzfi  43370  jm2.22  43423  jm2.23  43424  rmydioph  43442  expdioph  43451  rp-isfinite6  43945  relexpss1d  44132  relexpmulg  44137  iunrelexpmin2  44139  relexp0a  44143  relexpxpmin  44144  relexpaddss  44145  wallispilem3  46495  etransclem24  46686  lighneallem3  48070  lighneallem4  48073  nn0o1gt2ALTV  48170  nn0oALTV  48172  ztprmneprm  48823  blennn0elnn  49053  blen1b  49064  nn0sumshdiglem1  49097