Theorem elnn0 12451

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 12450	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2821	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 4119	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 11175	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 4632	. . 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 3915  {csn 4592  0cc0 11075  ℕcn 12193  ℕ₀cn0 12449

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 2702  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-mulcl 11137  ax-i2m1 11143

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 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-sn 4593  df-n0 12450

This theorem is referenced by:  0nn0  12464  nn0ge0  12474  nnnn0addcl  12479  nnm1nn0  12490  elnnnn0b  12493  nn0sub  12499  elnn0z  12549  elznn0nn  12550  elznn0  12551  elznn  12552  nn0lt10b  12603  nn0ind-raph  12641  nn0ledivnn  13073  expp1  14040  expneg  14041  expcllem  14044  znsqcld  14134  facp1  14250  faclbnd  14262  faclbnd3  14264  faclbnd4lem1  14265  faclbnd4lem3  14267  faclbnd4  14269  bcn1  14285  bcval5  14290  hashv01gt1  14317  hashnncl  14338  seqcoll2  14437  relexpsucl  15004  relexpsucr  15005  relexpcnv  15008  relexprelg  15011  relexpdmg  15015  relexprng  15019  relexpfld  15022  relexpaddg  15026  fz1f1o  15683  arisum  15833  arisum2  15834  pwdif  15841  geomulcvg  15849  fprodfac  15946  ef0lem  16051  nn0enne  16354  nn0o1gt2  16358  bezoutlem3  16518  dfgcd2  16523  mulgcd  16525  nn0rppwr  16538  nn0expgcd  16541  eucalgf  16560  eucalginv  16561  eucalglt  16562  prmdvdsexpr  16694  rpexp1i  16700  nn0gcdsq  16729  odzdvds  16773  pceq0  16849  fldivp1  16875  pockthg  16884  1arith  16905  4sqlem17  16939  4sqlem19  16941  vdwmc2  16957  vdwlem13  16971  0ram  16998  ram0  17000  ramz  17003  ramcl  17007  ressmulgnn0  19016  mulgnn0gsum  19019  mulgnn0p1  19024  mulgnn0subcl  19026  mulgneg  19031  mulgnn0z  19040  mulgnn0dir  19043  mulgnn0ass  19049  submmulg  19057  odcl  19473  mndodcongi  19480  oddvdsnn0  19481  odnncl  19482  oddvds  19484  dfod2  19501  odcl2  19502  gexcl  19517  gexdvds  19521  gexnnod  19525  sylow1lem1  19535  mulgnn0di  19762  torsubg  19791  ablfac1eu  20012  gzrngunitlem  21356  zringlpirlem3  21381  prmirredlem  21389  prmirred  21391  znf1o  21468  evlslem3  21994  dscmet  24467  dvexp2  25865  tdeglem4  25972  dgrnznn  26159  coefv0  26160  dgreq0  26178  dgrcolem2  26187  dvply1  26198  aaliou2  26255  radcnv0  26332  logfac  26517  logtayl  26576  cxpexp  26584  birthdaylem2  26869  harmonicbnd3  26925  sqf11  27056  ppiltx  27094  sqff1o  27099  lgsdir  27250  lgsabs1  27254  lgseisenlem1  27293  2sqlem7  27342  2sqblem  27349  2sqnn  27357  chebbnd1lem1  27387  nexple  32776  xrsmulgzz  32954  ressmulgnn0d  32992  fldext2rspun  33684  eulerpartlemsv2  34356  eulerpartlemv  34362  eulerpartlemb  34366  eulerpartlemf  34368  eulerpartlemgvv  34374  eulerpartlemgh  34376  fz0n  35725  bccolsum  35733  nn0prpw  36318  aks4d1p1  42071  sticksstones13  42154  negn0nposznnd  42277  dvdsexpnn0  42329  nn0addcom  42457  nn0mulcom  42461  zmulcomlem  42462  fsuppind  42585  fzsplit1nn0  42749  pell1qrgaplem  42868  monotoddzzfi  42938  jm2.22  42991  jm2.23  42992  rmydioph  43010  expdioph  43019  rp-isfinite6  43514  relexpss1d  43701  relexpmulg  43706  iunrelexpmin2  43708  relexp0a  43712  relexpxpmin  43713  relexpaddss  43714  wallispilem3  46072  etransclem24  46263  lighneallem3  47612  lighneallem4  47615  nn0o1gt2ALTV  47699  nn0oALTV  47701  ztprmneprm  48339  blennn0elnn  48570  blen1b  48581  nn0sumshdiglem1  48614