Theorem elnn0 12503

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 12502	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2826	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 4128	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 11229	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 4641	. . 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 2108   ∪ cun 3924  {csn 4601  0cc0 11129  ℕcn 12240  ℕ₀cn0 12501

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-1cn 11187  ax-icn 11188  ax-addcl 11189  ax-mulcl 11191  ax-i2m1 11197

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-sn 4602  df-n0 12502

This theorem is referenced by:  0nn0  12516  nn0ge0  12526  nnnn0addcl  12531  nnm1nn0  12542  elnnnn0b  12545  nn0sub  12551  elnn0z  12601  elznn0nn  12602  elznn0  12603  elznn  12604  nn0lt10b  12655  nn0ind-raph  12693  nn0ledivnn  13122  expp1  14086  expneg  14087  expcllem  14090  znsqcld  14180  facp1  14296  faclbnd  14308  faclbnd3  14310  faclbnd4lem1  14311  faclbnd4lem3  14313  faclbnd4  14315  bcn1  14331  bcval5  14336  hashv01gt1  14363  hashnncl  14384  seqcoll2  14483  relexpsucl  15050  relexpsucr  15051  relexpcnv  15054  relexprelg  15057  relexpdmg  15061  relexprng  15065  relexpfld  15068  relexpaddg  15072  fz1f1o  15726  arisum  15876  arisum2  15877  pwdif  15884  geomulcvg  15892  fprodfac  15989  ef0lem  16094  nn0enne  16396  nn0o1gt2  16400  bezoutlem3  16560  dfgcd2  16565  mulgcd  16567  nn0rppwr  16580  nn0expgcd  16583  eucalgf  16602  eucalginv  16603  eucalglt  16604  prmdvdsexpr  16736  rpexp1i  16742  nn0gcdsq  16771  odzdvds  16815  pceq0  16891  fldivp1  16917  pockthg  16926  1arith  16947  4sqlem17  16981  4sqlem19  16983  vdwmc2  16999  vdwlem13  17013  0ram  17040  ram0  17042  ramz  17045  ramcl  17049  ressmulgnn0  19060  mulgnn0gsum  19063  mulgnn0p1  19068  mulgnn0subcl  19070  mulgneg  19075  mulgnn0z  19084  mulgnn0dir  19087  mulgnn0ass  19093  submmulg  19101  odcl  19517  mndodcongi  19524  oddvdsnn0  19525  odnncl  19526  oddvds  19528  dfod2  19545  odcl2  19546  gexcl  19561  gexdvds  19565  gexnnod  19569  sylow1lem1  19579  mulgnn0di  19806  torsubg  19835  ablfac1eu  20056  gzrngunitlem  21400  zringlpirlem3  21425  prmirredlem  21433  prmirred  21435  znf1o  21512  evlslem3  22038  dscmet  24511  dvexp2  25910  tdeglem4  26017  dgrnznn  26204  coefv0  26205  dgreq0  26223  dgrcolem2  26232  dvply1  26243  aaliou2  26300  radcnv0  26377  logfac  26562  logtayl  26621  cxpexp  26629  birthdaylem2  26914  harmonicbnd3  26970  sqf11  27101  ppiltx  27139  sqff1o  27144  lgsdir  27295  lgsabs1  27299  lgseisenlem1  27338  2sqlem7  27387  2sqblem  27394  2sqnn  27402  chebbnd1lem1  27432  nexple  32823  xrsmulgzz  33001  ressmulgnn0d  33039  fldext2rspun  33723  eulerpartlemsv2  34390  eulerpartlemv  34396  eulerpartlemb  34400  eulerpartlemf  34402  eulerpartlemgvv  34408  eulerpartlemgh  34410  fz0n  35748  bccolsum  35756  nn0prpw  36341  aks4d1p1  42089  sticksstones13  42172  negn0nposznnd  42332  dvdsexpnn0  42383  nn0addcom  42493  nn0mulcom  42497  zmulcomlem  42498  fsuppind  42613  fzsplit1nn0  42777  pell1qrgaplem  42896  monotoddzzfi  42966  jm2.22  43019  jm2.23  43020  rmydioph  43038  expdioph  43047  rp-isfinite6  43542  relexpss1d  43729  relexpmulg  43734  iunrelexpmin2  43736  relexp0a  43740  relexpxpmin  43741  relexpaddss  43742  wallispilem3  46096  etransclem24  46287  lighneallem3  47621  lighneallem4  47624  nn0o1gt2ALTV  47708  nn0oALTV  47710  ztprmneprm  48322  blennn0elnn  48557  blen1b  48568  nn0sumshdiglem1  48601