Theorem elnn0 11887

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 11886	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2881	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 4076	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 10624	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 4564	. . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0)
6	5	orbi2i 910	. 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
7	2, 3, 6	3bitri 300	1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

Syntax hints:   ↔ wb 209   ∨ wo 844   = wceq 1538   ∈ wcel 2111   ∪ cun 3879  {csn 4525  0cc0 10526  ℕcn 11625  ℕ₀cn0 11885

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-mulcl 10588  ax-i2m1 10594

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-n0 11886

This theorem is referenced by:  0nn0  11900  nn0ge0  11910  nnnn0addcl  11915  nnm1nn0  11926  elnnnn0b  11929  nn0sub  11935  elnn0z  11982  elznn0nn  11983  elznn0  11984  elznn  11985  nn0lt10b  12032  nn0ind-raph  12070  nn0ledivnn  12490  expp1  13432  expneg  13433  expcllem  13436  znsqcld  13522  facp1  13634  faclbnd  13646  faclbnd3  13648  faclbnd4lem1  13649  faclbnd4lem3  13651  faclbnd4  13653  bcn1  13669  bcval5  13674  hashv01gt1  13701  hashnncl  13723  seqcoll2  13819  relexpsucl  14382  relexpsucr  14383  relexpcnv  14386  relexprelg  14389  relexpdmg  14393  relexprng  14397  relexpfld  14400  relexpaddg  14404  fz1f1o  15059  arisum  15207  arisum2  15208  pwdif  15215  geomulcvg  15224  fprodfac  15319  ef0lem  15424  nn0enne  15718  nn0o1gt2  15722  bezoutlem3  15879  dfgcd2  15884  mulgcd  15886  eucalgf  15917  eucalginv  15918  eucalglt  15919  prmdvdsexpr  16051  rpexp1i  16055  nn0gcdsq  16082  odzdvds  16122  pceq0  16197  fldivp1  16223  pockthg  16232  1arith  16253  4sqlem17  16287  4sqlem19  16289  vdwmc2  16305  vdwlem13  16319  0ram  16346  ram0  16348  ramz  16351  ramcl  16355  mulgnn0gsum  18226  mulgnn0p1  18231  mulgnn0subcl  18233  mulgneg  18238  mulgnn0z  18246  mulgnn0dir  18249  mulgnn0ass  18255  submmulg  18263  odcl  18656  mndodcongi  18663  oddvdsnn0  18664  odnncl  18665  oddvds  18667  dfod2  18683  odcl2  18684  gexcl  18697  gexdvds  18701  gexnnod  18705  sylow1lem1  18715  mulgnn0di  18939  torsubg  18967  ablfac1eu  19188  gzrngunitlem  20156  zringlpirlem3  20179  prmirredlem  20186  prmirred  20188  znf1o  20243  evlslem3  20752  dscmet  23179  dvexp2  24557  tdeglem4  24661  dgrnznn  24844  coefv0  24845  dgreq0  24862  dgrcolem2  24871  dvply1  24880  aaliou2  24936  radcnv0  25011  logfac  25192  logtayl  25251  cxpexp  25259  birthdaylem2  25538  harmonicbnd3  25593  sqf11  25724  ppiltx  25762  sqff1o  25767  lgsdir  25916  lgsabs1  25920  lgseisenlem1  25959  2sqlem7  26008  2sqblem  26015  2sqnn  26023  chebbnd1lem1  26053  xrsmulgzz  30712  ressmulgnn0  30718  nexple  31378  eulerpartlemsv2  31726  eulerpartlemv  31732  eulerpartlemb  31736  eulerpartlemf  31738  eulerpartlemgvv  31744  eulerpartlemgh  31746  fz0n  33075  bccolsum  33084  nn0prpw  33784  fsuppind  39456  negn0nposznnd  39476  nn0rppwr  39490  nn0expgcd  39492  fzsplit1nn0  39695  pell1qrgaplem  39814  monotoddzzfi  39883  jm2.22  39936  jm2.23  39937  rmydioph  39955  expdioph  39964  rp-isfinite6  40226  relexpss1d  40406  relexpmulg  40411  iunrelexpmin2  40413  relexp0a  40417  relexpxpmin  40418  relexpaddss  40419  wallispilem3  42709  etransclem24  42900  lighneallem3  44125  lighneallem4  44128  nn0o1gt2ALTV  44212  nn0oALTV  44214  ztprmneprm  44749  blennn0elnn  44991  blen1b  45002  nn0sumshdiglem1  45035