Theorem elnn0 12092

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 12091	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2829	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 4063	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 10827	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 4580	. . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0)
6	5	orbi2i 913	. 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
7	2, 3, 6	3bitri 300	1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

Syntax hints:   ↔ wb 209   ∨ wo 847   = wceq 1543   ∈ wcel 2110   ∪ cun 3864  {csn 4541  0cc0 10729  ℕcn 11830  ℕ₀cn0 12090

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-mulcl 10791  ax-i2m1 10797

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-un 3871  df-sn 4542  df-n0 12091

This theorem is referenced by:  0nn0  12105  nn0ge0  12115  nnnn0addcl  12120  nnm1nn0  12131  elnnnn0b  12134  nn0sub  12140  elnn0z  12189  elznn0nn  12190  elznn0  12191  elznn  12192  nn0lt10b  12239  nn0ind-raph  12277  nn0ledivnn  12699  expp1  13642  expneg  13643  expcllem  13646  znsqcld  13732  facp1  13844  faclbnd  13856  faclbnd3  13858  faclbnd4lem1  13859  faclbnd4lem3  13861  faclbnd4  13863  bcn1  13879  bcval5  13884  hashv01gt1  13911  hashnncl  13933  seqcoll2  14031  relexpsucl  14594  relexpsucr  14595  relexpcnv  14598  relexprelg  14601  relexpdmg  14605  relexprng  14609  relexpfld  14612  relexpaddg  14616  fz1f1o  15274  arisum  15424  arisum2  15425  pwdif  15432  geomulcvg  15440  fprodfac  15535  ef0lem  15640  nn0enne  15938  nn0o1gt2  15942  bezoutlem3  16101  dfgcd2  16106  mulgcd  16108  eucalgf  16140  eucalginv  16141  eucalglt  16142  prmdvdsexpr  16274  rpexp1i  16280  nn0gcdsq  16308  odzdvds  16348  pceq0  16424  fldivp1  16450  pockthg  16459  1arith  16480  4sqlem17  16514  4sqlem19  16516  vdwmc2  16532  vdwlem13  16546  0ram  16573  ram0  16575  ramz  16578  ramcl  16582  mulgnn0gsum  18498  mulgnn0p1  18503  mulgnn0subcl  18505  mulgneg  18510  mulgnn0z  18518  mulgnn0dir  18521  mulgnn0ass  18527  submmulg  18535  odcl  18928  mndodcongi  18935  oddvdsnn0  18936  odnncl  18937  oddvds  18939  dfod2  18955  odcl2  18956  gexcl  18969  gexdvds  18973  gexnnod  18977  sylow1lem1  18987  mulgnn0di  19211  torsubg  19239  ablfac1eu  19460  gzrngunitlem  20428  zringlpirlem3  20451  prmirredlem  20459  prmirred  20461  znf1o  20516  evlslem3  21040  dscmet  23470  dvexp2  24851  tdeglem4  24957  tdeglem4OLD  24958  dgrnznn  25141  coefv0  25142  dgreq0  25159  dgrcolem2  25168  dvply1  25177  aaliou2  25233  radcnv0  25308  logfac  25489  logtayl  25548  cxpexp  25556  birthdaylem2  25835  harmonicbnd3  25890  sqf11  26021  ppiltx  26059  sqff1o  26064  lgsdir  26213  lgsabs1  26217  lgseisenlem1  26256  2sqlem7  26305  2sqblem  26312  2sqnn  26320  chebbnd1lem1  26350  xrsmulgzz  31006  ressmulgnn0  31012  nexple  31689  eulerpartlemsv2  32037  eulerpartlemv  32043  eulerpartlemb  32047  eulerpartlemf  32049  eulerpartlemgvv  32055  eulerpartlemgh  32057  fz0n  33414  bccolsum  33423  nn0prpw  34249  aks4d1p1  39817  sticksstones13  39837  fsuppind  39989  negn0nposznnd  40017  nn0rppwr  40041  nn0expgcd  40043  dvdsexpnn0  40049  fzsplit1nn0  40279  pell1qrgaplem  40398  monotoddzzfi  40467  jm2.22  40520  jm2.23  40521  rmydioph  40539  expdioph  40548  rp-isfinite6  40810  relexpss1d  40990  relexpmulg  40995  iunrelexpmin2  40997  relexp0a  41001  relexpxpmin  41002  relexpaddss  41003  wallispilem3  43283  etransclem24  43474  lighneallem3  44732  lighneallem4  44735  nn0o1gt2ALTV  44819  nn0oALTV  44821  ztprmneprm  45356  blennn0elnn  45596  blen1b  45607  nn0sumshdiglem1  45640