Theorem elnn0 12477

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 12476	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2853	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 4104	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 11167	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 4621	. . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0)
6	5	orbi2i 923	. 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
7	2, 3, 6	3bitri 299	1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

Syntax hints:   ↔ wb 208   ∨ wo 858   = wceq 1559   ∈ wcel 2141   ∪ cun 3900  {csn 4579  0cc0 11067  ℕcn 12204  ℕ₀cn0 12475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-1cn 11125  ax-icn 11126  ax-addcl 11127  ax-mulcl 11129  ax-i2m1 11135

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3907  df-sn 4580  df-n0 12476

This theorem is referenced by:  0nn0  12490  nn0ge0  12500  nnnn0addcl  12505  nnm1nn0  12516  elnnnn0b  12519  nn0sub  12525  elnn0z  12575  elznn0nn  12576  elznn0  12577  elznn  12578  nn0lt10b  12629  nn0ind-raph  12667  nn0ledivnn  13102  expp1  14075  expneg  14076  expcllem  14079  znsqcld  14169  facp1  14285  faclbnd  14297  faclbnd3  14299  faclbnd4lem1  14300  faclbnd4lem3  14302  faclbnd4  14304  bcn1  14320  bcval5  14325  hashv01gt1  14352  hashnncl  14373  seqcoll2  14472  relexpsucl  15038  relexpsucr  15039  relexpcnv  15042  relexprelg  15045  relexpdmg  15049  relexprng  15053  relexpfld  15056  relexpaddg  15060  fz1f1o  15728  arisum  15881  arisum2  15882  pwdif  15889  geomulcvg  15897  fprodfac  15994  ef0lem  16099  nn0enne  16402  nn0o1gt2  16406  bezoutlem3  16566  dfgcd2  16571  mulgcd  16573  nn0rppwr  16586  nn0expgcd  16589  eucalgf  16608  eucalginv  16609  eucalglt  16610  prmdvdsexpr  16743  rpexp1i  16749  nn0gcdsq  16778  odzdvds  16822  pceq0  16898  fldivp1  16924  pockthg  16933  1arith  16954  4sqlem17  16988  4sqlem19  16990  vdwmc2  17006  vdwlem13  17020  0ram  17047  ram0  17049  ramz  17052  ramcl  17056  ressmulgnn0  19110  mulgnn0gsum  19113  mulgnn0p1  19118  mulgnn0subcl  19120  mulgneg  19125  mulgnn0z  19134  mulgnn0dir  19137  mulgnn0ass  19143  submmulg  19151  odcl  19567  mndodcongi  19574  oddvdsnn0  19575  odnncl  19576  oddvds  19578  dfod2  19595  odcl2  19596  gexcl  19611  gexdvds  19615  gexnnod  19619  sylow1lem1  19629  mulgnn0di  19856  torsubg  19885  ablfac1eu  20106  gzrngunitlem  21472  zringlpirlem3  21504  prmirredlem  21512  prmirred  21514  znf1o  21591  evlslem3  22121  dscmet  24620  dvexp2  26004  tdeglem4  26108  dgrnznn  26295  coefv0  26296  dgreq0  26313  dgrcolem2  26322  dvply1  26336  aaliou2  26392  radcnv0  26467  logfac  26654  logtayl  26713  cxpexp  26721  birthdaylem2  27005  harmonicbnd3  27060  sqf11  27191  ppiltx  27229  sqff1o  27234  lgsdir  27384  lgsabs1  27388  lgseisenlem1  27427  2sqlem7  27476  2sqblem  27483  2sqnn  27491  chebbnd1lem1  27521  nexple  32996  xrsmulgzz  33148  ressmulgnn0d  33185  fldext2rspun  33940  eulerpartlemsv2  34616  eulerpartlemv  34622  eulerpartlemb  34626  eulerpartlemf  34628  eulerpartlemgvv  34634  eulerpartlemgh  34636  fz0n  36042  bccolsum  36050  nn0prpw  36644  aks4d1p1  42654  sticksstones13  42737  negn0nposznnd  42852  dvdsexpnn0  42904  nn0addcom  43045  nn0mulcom  43049  zmulcomlem  43050  fsuppind  43133  fzsplit1nn0  43296  pell1qrgaplem  43411  monotoddzzfi  43480  jm2.22  43533  jm2.23  43534  rmydioph  43552  expdioph  43561  rp-isfinite6  44055  relexpss1d  44242  relexpmulg  44247  iunrelexpmin2  44249  relexp0a  44253  relexpxpmin  44254  relexpaddss  44255  wallispilem3  46602  etransclem24  46793  lighneallem3  48177  lighneallem4  48180  nn0o1gt2ALTV  48277  nn0oALTV  48279  ztprmneprm  48930  blennn0elnn  49160  blen1b  49171  nn0sumshdiglem1  49204