Theorem elnn0 12474

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 12473	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2826	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 4149	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 11208	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 4668	. . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0)
6	5	orbi2i 912	. 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
7	2, 3, 6	3bitri 297	1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

Syntax hints:   ↔ wb 205   ∨ wo 846   = wceq 1542   ∈ wcel 2107   ∪ cun 3947  {csn 4629  0cc0 11110  ℕcn 12212  ℕ₀cn0 12472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-mulcl 11172  ax-i2m1 11178

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-sn 4630  df-n0 12473

This theorem is referenced by:  0nn0  12487  nn0ge0  12497  nnnn0addcl  12502  nnm1nn0  12513  elnnnn0b  12516  nn0sub  12522  elnn0z  12571  elznn0nn  12572  elznn0  12573  elznn  12574  nn0lt10b  12624  nn0ind-raph  12662  nn0ledivnn  13087  expp1  14034  expneg  14035  expcllem  14038  znsqcld  14127  facp1  14238  faclbnd  14250  faclbnd3  14252  faclbnd4lem1  14253  faclbnd4lem3  14255  faclbnd4  14257  bcn1  14273  bcval5  14278  hashv01gt1  14305  hashnncl  14326  seqcoll2  14426  relexpsucl  14978  relexpsucr  14979  relexpcnv  14982  relexprelg  14985  relexpdmg  14989  relexprng  14993  relexpfld  14996  relexpaddg  15000  fz1f1o  15656  arisum  15806  arisum2  15807  pwdif  15814  geomulcvg  15822  fprodfac  15917  ef0lem  16022  nn0enne  16320  nn0o1gt2  16324  bezoutlem3  16483  dfgcd2  16488  mulgcd  16490  eucalgf  16520  eucalginv  16521  eucalglt  16522  prmdvdsexpr  16654  rpexp1i  16660  nn0gcdsq  16688  odzdvds  16728  pceq0  16804  fldivp1  16830  pockthg  16839  1arith  16860  4sqlem17  16894  4sqlem19  16896  vdwmc2  16912  vdwlem13  16926  0ram  16953  ram0  16955  ramz  16958  ramcl  16962  mulgnn0gsum  18960  mulgnn0p1  18965  mulgnn0subcl  18967  mulgneg  18972  mulgnn0z  18981  mulgnn0dir  18984  mulgnn0ass  18990  submmulg  18998  odcl  19404  mndodcongi  19411  oddvdsnn0  19412  odnncl  19413  oddvds  19415  dfod2  19432  odcl2  19433  gexcl  19448  gexdvds  19452  gexnnod  19456  sylow1lem1  19466  mulgnn0di  19693  torsubg  19722  ablfac1eu  19943  gzrngunitlem  21010  zringlpirlem3  21034  prmirredlem  21042  prmirred  21044  znf1o  21107  evlslem3  21643  dscmet  24081  dvexp2  25471  tdeglem4  25577  tdeglem4OLD  25578  dgrnznn  25761  coefv0  25762  dgreq0  25779  dgrcolem2  25788  dvply1  25797  aaliou2  25853  radcnv0  25928  logfac  26109  logtayl  26168  cxpexp  26176  birthdaylem2  26457  harmonicbnd3  26512  sqf11  26643  ppiltx  26681  sqff1o  26686  lgsdir  26835  lgsabs1  26839  lgseisenlem1  26878  2sqlem7  26927  2sqblem  26934  2sqnn  26942  chebbnd1lem1  26972  xrsmulgzz  32179  ressmulgnn0  32185  nexple  33007  eulerpartlemsv2  33357  eulerpartlemv  33363  eulerpartlemb  33367  eulerpartlemf  33369  eulerpartlemgvv  33375  eulerpartlemgh  33377  fz0n  34700  bccolsum  34709  nn0prpw  35208  aks4d1p1  40941  sticksstones13  40975  fsuppind  41162  negn0nposznnd  41194  nn0rppwr  41224  nn0expgcd  41226  dvdsexpnn0  41232  nn0addcom  41323  nn0mulcom  41327  zmulcomlem  41328  fzsplit1nn0  41492  pell1qrgaplem  41611  monotoddzzfi  41681  jm2.22  41734  jm2.23  41735  rmydioph  41753  expdioph  41762  rp-isfinite6  42269  relexpss1d  42456  relexpmulg  42461  iunrelexpmin2  42463  relexp0a  42467  relexpxpmin  42468  relexpaddss  42469  wallispilem3  44783  etransclem24  44974  lighneallem3  46275  lighneallem4  46278  nn0o1gt2ALTV  46362  nn0oALTV  46364  ztprmneprm  47023  blennn0elnn  47263  blen1b  47274  nn0sumshdiglem1  47307