Theorem elnn0 12405

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 12404	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2820	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 4106	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 11128	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 4619	. . 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 3903  {csn 4579  0cc0 11028  ℕcn 12147  ℕ₀cn0 12403

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 11086  ax-icn 11087  ax-addcl 11088  ax-mulcl 11090  ax-i2m1 11096

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 3440  df-un 3910  df-sn 4580  df-n0 12404

This theorem is referenced by:  0nn0  12418  nn0ge0  12428  nnnn0addcl  12433  nnm1nn0  12444  elnnnn0b  12447  nn0sub  12453  elnn0z  12503  elznn0nn  12504  elznn0  12505  elznn  12506  nn0lt10b  12557  nn0ind-raph  12595  nn0ledivnn  13027  expp1  13994  expneg  13995  expcllem  13998  znsqcld  14088  facp1  14204  faclbnd  14216  faclbnd3  14218  faclbnd4lem1  14219  faclbnd4lem3  14221  faclbnd4  14223  bcn1  14239  bcval5  14244  hashv01gt1  14271  hashnncl  14292  seqcoll2  14391  relexpsucl  14957  relexpsucr  14958  relexpcnv  14961  relexprelg  14964  relexpdmg  14968  relexprng  14972  relexpfld  14975  relexpaddg  14979  fz1f1o  15636  arisum  15786  arisum2  15787  pwdif  15794  geomulcvg  15802  fprodfac  15899  ef0lem  16004  nn0enne  16307  nn0o1gt2  16311  bezoutlem3  16471  dfgcd2  16476  mulgcd  16478  nn0rppwr  16491  nn0expgcd  16494  eucalgf  16513  eucalginv  16514  eucalglt  16515  prmdvdsexpr  16647  rpexp1i  16653  nn0gcdsq  16682  odzdvds  16726  pceq0  16802  fldivp1  16828  pockthg  16837  1arith  16858  4sqlem17  16892  4sqlem19  16894  vdwmc2  16910  vdwlem13  16924  0ram  16951  ram0  16953  ramz  16956  ramcl  16960  ressmulgnn0  18975  mulgnn0gsum  18978  mulgnn0p1  18983  mulgnn0subcl  18985  mulgneg  18990  mulgnn0z  18999  mulgnn0dir  19002  mulgnn0ass  19008  submmulg  19016  odcl  19434  mndodcongi  19441  oddvdsnn0  19442  odnncl  19443  oddvds  19445  dfod2  19462  odcl2  19463  gexcl  19478  gexdvds  19482  gexnnod  19486  sylow1lem1  19496  mulgnn0di  19723  torsubg  19752  ablfac1eu  19973  gzrngunitlem  21358  zringlpirlem3  21390  prmirredlem  21398  prmirred  21400  znf1o  21477  evlslem3  22004  dscmet  24477  dvexp2  25875  tdeglem4  25982  dgrnznn  26169  coefv0  26170  dgreq0  26188  dgrcolem2  26197  dvply1  26208  aaliou2  26265  radcnv0  26342  logfac  26527  logtayl  26586  cxpexp  26594  birthdaylem2  26879  harmonicbnd3  26935  sqf11  27066  ppiltx  27104  sqff1o  27109  lgsdir  27260  lgsabs1  27264  lgseisenlem1  27303  2sqlem7  27352  2sqblem  27359  2sqnn  27367  chebbnd1lem1  27397  nexple  32808  xrsmulgzz  32982  ressmulgnn0d  33017  fldext2rspun  33668  eulerpartlemsv2  34345  eulerpartlemv  34351  eulerpartlemb  34355  eulerpartlemf  34357  eulerpartlemgvv  34363  eulerpartlemgh  34365  fz0n  35723  bccolsum  35731  nn0prpw  36316  aks4d1p1  42069  sticksstones13  42152  negn0nposznnd  42275  dvdsexpnn0  42327  nn0addcom  42455  nn0mulcom  42459  zmulcomlem  42460  fsuppind  42583  fzsplit1nn0  42747  pell1qrgaplem  42866  monotoddzzfi  42935  jm2.22  42988  jm2.23  42989  rmydioph  43007  expdioph  43016  rp-isfinite6  43511  relexpss1d  43698  relexpmulg  43703  iunrelexpmin2  43705  relexp0a  43709  relexpxpmin  43710  relexpaddss  43711  wallispilem3  46068  etransclem24  46259  lighneallem3  47611  lighneallem4  47614  nn0o1gt2ALTV  47698  nn0oALTV  47700  ztprmneprm  48351  blennn0elnn  48582  blen1b  48593  nn0sumshdiglem1  48626