Theorem elnn0 12386

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 12385	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2820	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 4104	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 11109	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 4617	. . 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 3901  {csn 4577  0cc0 11009  ℕcn 12128  ℕ₀cn0 12384

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 11067  ax-icn 11068  ax-addcl 11069  ax-mulcl 11071  ax-i2m1 11077

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 3438  df-un 3908  df-sn 4578  df-n0 12385

This theorem is referenced by:  0nn0  12399  nn0ge0  12409  nnnn0addcl  12414  nnm1nn0  12425  elnnnn0b  12428  nn0sub  12434  elnn0z  12484  elznn0nn  12485  elznn0  12486  elznn  12487  nn0lt10b  12538  nn0ind-raph  12576  nn0ledivnn  13008  expp1  13975  expneg  13976  expcllem  13979  znsqcld  14069  facp1  14185  faclbnd  14197  faclbnd3  14199  faclbnd4lem1  14200  faclbnd4lem3  14202  faclbnd4  14204  bcn1  14220  bcval5  14225  hashv01gt1  14252  hashnncl  14273  seqcoll2  14372  relexpsucl  14938  relexpsucr  14939  relexpcnv  14942  relexprelg  14945  relexpdmg  14949  relexprng  14953  relexpfld  14956  relexpaddg  14960  fz1f1o  15617  arisum  15767  arisum2  15768  pwdif  15775  geomulcvg  15783  fprodfac  15880  ef0lem  15985  nn0enne  16288  nn0o1gt2  16292  bezoutlem3  16452  dfgcd2  16457  mulgcd  16459  nn0rppwr  16472  nn0expgcd  16475  eucalgf  16494  eucalginv  16495  eucalglt  16496  prmdvdsexpr  16628  rpexp1i  16634  nn0gcdsq  16663  odzdvds  16707  pceq0  16783  fldivp1  16809  pockthg  16818  1arith  16839  4sqlem17  16873  4sqlem19  16875  vdwmc2  16891  vdwlem13  16905  0ram  16932  ram0  16934  ramz  16937  ramcl  16941  ressmulgnn0  18956  mulgnn0gsum  18959  mulgnn0p1  18964  mulgnn0subcl  18966  mulgneg  18971  mulgnn0z  18980  mulgnn0dir  18983  mulgnn0ass  18989  submmulg  18997  odcl  19415  mndodcongi  19422  oddvdsnn0  19423  odnncl  19424  oddvds  19426  dfod2  19443  odcl2  19444  gexcl  19459  gexdvds  19463  gexnnod  19467  sylow1lem1  19477  mulgnn0di  19704  torsubg  19733  ablfac1eu  19954  gzrngunitlem  21339  zringlpirlem3  21371  prmirredlem  21379  prmirred  21381  znf1o  21458  evlslem3  21985  dscmet  24458  dvexp2  25856  tdeglem4  25963  dgrnznn  26150  coefv0  26151  dgreq0  26169  dgrcolem2  26178  dvply1  26189  aaliou2  26246  radcnv0  26323  logfac  26508  logtayl  26567  cxpexp  26575  birthdaylem2  26860  harmonicbnd3  26916  sqf11  27047  ppiltx  27085  sqff1o  27090  lgsdir  27241  lgsabs1  27245  lgseisenlem1  27284  2sqlem7  27333  2sqblem  27340  2sqnn  27348  chebbnd1lem1  27378  nexple  32790  xrsmulgzz  32964  ressmulgnn0d  32999  fldext2rspun  33655  eulerpartlemsv2  34332  eulerpartlemv  34338  eulerpartlemb  34342  eulerpartlemf  34344  eulerpartlemgvv  34350  eulerpartlemgh  34352  fz0n  35714  bccolsum  35722  nn0prpw  36307  aks4d1p1  42059  sticksstones13  42142  negn0nposznnd  42265  dvdsexpnn0  42317  nn0addcom  42445  nn0mulcom  42449  zmulcomlem  42450  fsuppind  42573  fzsplit1nn0  42737  pell1qrgaplem  42856  monotoddzzfi  42925  jm2.22  42978  jm2.23  42979  rmydioph  42997  expdioph  43006  rp-isfinite6  43501  relexpss1d  43688  relexpmulg  43693  iunrelexpmin2  43695  relexp0a  43699  relexpxpmin  43700  relexpaddss  43701  wallispilem3  46058  etransclem24  46249  lighneallem3  47601  lighneallem4  47604  nn0o1gt2ALTV  47688  nn0oALTV  47690  ztprmneprm  48341  blennn0elnn  48572  blen1b  48583  nn0sumshdiglem1  48616