Theorem elnn0 12501

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 12500	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2855	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 4107	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 11195	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 4631	. . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0)
6	5	orbi2i 925	. 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
7	2, 3, 6	3bitri 300	1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

Syntax hints:   ↔ wb 209   ∨ wo 860   = wceq 1570   ∈ wcel 2143   ∪ cun 3903  {csn 4589  0cc0 11095  ℕcn 12228  ℕ₀cn0 12499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-mulcl 11157  ax-i2m1 11163

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910  df-sn 4590  df-n0 12500

This theorem is referenced by:  0nn0  12514  nn0ge0  12524  nnnn0addcl  12529  nnm1nn0  12540  elnnnn0b  12543  nn0sub  12549  elnn0z  12599  elznn0nn  12600  elznn0  12601  elznn  12602  nn0lt10b  12653  nn0ind-raph  12691  nn0ledivnn  13126  expp1  14100  expneg  14101  expcllem  14104  znsqcld  14194  facp1  14310  faclbnd  14322  faclbnd3  14324  faclbnd4lem1  14325  faclbnd4lem3  14327  faclbnd4  14329  bcn1  14345  bcval5  14350  hashv01gt1  14377  hashnncl  14398  seqcoll2  14498  relexpsucl  15064  relexpsucr  15065  relexpcnv  15068  relexprelg  15071  relexpdmg  15075  relexprng  15079  relexpfld  15082  relexpaddg  15086  fz1f1o  15757  arisum  15910  arisum2  15911  pwdif  15918  geomulcvg  15926  fprodfac  16023  ef0lem  16127  nn0enne  16430  nn0o1gt2  16434  bezoutlem3  16594  dfgcd2  16599  mulgcd  16601  nn0rppwr  16614  nn0expgcd  16617  eucalgf  16636  eucalginv  16637  eucalglt  16638  prmdvdsexpr  16771  rpexp1i  16777  nn0gcdsq  16806  odzdvds  16850  pceq0  16926  fldivp1  16952  pockthg  16961  1arith  16982  4sqlem17  17016  4sqlem19  17018  vdwmc2  17034  vdwlem13  17048  0ram  17075  ram0  17077  ramz  17080  ramcl  17084  ressmulgnn0  19138  mulgnn0gsum  19141  mulgnn0p1  19146  mulgnn0subcl  19148  mulgneg  19153  mulgnn0z  19162  mulgnn0dir  19165  mulgnn0ass  19171  submmulg  19179  odcl  19601  mndodcongi  19608  oddvdsnn0  19609  odnncl  19610  oddvds  19612  dfod2  19629  odcl2  19630  gexcl  19645  gexdvds  19649  gexnnod  19653  sylow1lem1  19663  mulgnn0di  19890  torsubg  19919  ablfac1eu  20140  gzrngunitlem  21582  zringlpirlem3  21614  prmirredlem  21622  prmirred  21624  znf1o  21701  evlslem3  22231  dscmet  24729  dvexp2  26113  tdeglem4  26217  dgrnznn  26404  coefv0  26405  dgreq0  26422  dgrcolem2  26431  dvply1  26445  aaliou2  26503  radcnv0  26579  logfac  26766  logtayl  26825  cxpexp  26833  birthdaylem2  27117  harmonicbnd3  27172  sqf11  27303  ppiltx  27341  sqff1o  27346  lgsdir  27496  lgsabs1  27500  lgseisenlem1  27539  2sqlem7  27588  2sqblem  27595  2sqnn  27603  chebbnd1lem1  27633  nexple  33177  xrsmulgzz  33329  ressmulgnn0d  33364  fldext2rspun  34072  eulerpartlemsv2  34748  eulerpartlemv  34754  eulerpartlemb  34758  eulerpartlemf  34760  eulerpartlemgvv  34766  eulerpartlemgh  34768  fz0n  36223  bccolsum  36231  nn0prpw  36834  aks4d1p1  42843  sticksstones13  42926  negn0nposznnd  43043  dvdsexpnn0  43095  nn0addcom  43236  nn0mulcom  43240  zmulcomlem  43241  fsuppind  43322  fzsplit1nn0  43485  pell1qrgaplem  43600  monotoddzzfi  43669  jm2.22  43722  jm2.23  43723  rmydioph  43741  expdioph  43750  rp-isfinite6  44244  relexpss1d  44431  relexpmulg  44436  iunrelexpmin2  44438  relexp0a  44442  relexpxpmin  44443  relexpaddss  44444  wallispilem3  46781  etransclem24  46972  lighneallem3  48359  lighneallem4  48362  nn0o1gt2ALTV  48459  nn0oALTV  48461  ztprmneprm  49127  blennn0elnn  49357  blen1b  49368  nn0sumshdiglem1  49401