Theorem elnn0 11619

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 11618	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2897	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 3979	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 10349	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 4431	. . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0)
6	5	orbi2i 943	. 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
7	2, 3, 6	3bitri 289	1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

Syntax hints:   ↔ wb 198   ∨ wo 880   = wceq 1658   ∈ wcel 2166   ∪ cun 3795  {csn 4396  0cc0 10251  ℕcn 11349  ℕ₀cn0 11617

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2802  ax-1cn 10309  ax-icn 10310  ax-addcl 10311  ax-mulcl 10313  ax-i2m1 10319

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-v 3415  df-un 3802  df-sn 4397  df-n0 11618

This theorem is referenced by:  0nn0  11634  nn0ge0  11644  nnnn0addcl  11649  nnm1nn0  11660  elnnnn0b  11663  nn0sub  11669  elnn0z  11716  elznn0nn  11717  elznn0  11718  elznn  11719  nn0lt10b  11766  nn0ind-raph  11804  nn0ledivnn  12226  expp1  13160  expneg  13161  expcllem  13164  facp1  13357  faclbnd  13369  faclbnd3  13371  faclbnd4lem1  13372  faclbnd4lem3  13374  faclbnd4  13376  bcn1  13392  bcval5  13397  hashv01gt1  13424  hashnncl  13446  seqcoll2  13537  relexpsucr  14145  relexpsucl  14149  relexpcnv  14151  relexprelg  14154  relexpdmg  14158  relexprng  14162  relexpfld  14165  relexpaddg  14169  fz1f1o  14817  arisum  14965  arisum2  14966  geomulcvg  14980  fprodfac  15075  ef0lem  15180  nn0enne  15467  nn0o1gt2  15470  bezoutlem3  15630  dfgcd2  15635  mulgcd  15637  eucalgf  15668  eucalginv  15669  eucalglt  15670  prmdvdsexpr  15799  rpexp1i  15803  nn0gcdsq  15830  odzdvds  15870  pceq0  15945  fldivp1  15971  pockthg  15980  1arith  16001  4sqlem17  16035  4sqlem19  16037  vdwmc2  16053  vdwlem13  16067  0ram  16094  ram0  16096  ramz  16099  ramcl  16103  mulgnn0p1  17905  mulgnn0subcl  17907  mulgneg  17912  mulgnn0z  17919  mulgnn0dir  17922  mulgnn0ass  17928  submmulg  17936  odcl  18305  mndodcongi  18312  oddvdsnn0  18313  odnncl  18314  oddvds  18316  dfod2  18331  odcl2  18332  gexcl  18345  gexdvds  18349  gexnnod  18353  sylow1lem1  18363  mulgnn0di  18583  torsubg  18609  ablfac1eu  18825  evlslem3  19873  gzrngunitlem  20170  zringlpirlem3  20193  prmirredlem  20200  prmirred  20202  znf1o  20258  dscmet  22746  dvexp2  24115  tdeglem4  24218  dgrnznn  24401  coefv0  24402  dgreq0  24419  dgrcolem2  24428  dvply1  24437  aaliou2  24493  radcnv0  24568  logfac  24745  logtayl  24804  cxpexp  24812  leibpilem1  25079  birthdaylem2  25091  harmonicbnd3  25146  sqf11  25277  ppiltx  25315  sqff1o  25320  lgsdir  25469  lgsabs1  25473  lgseisenlem1  25512  2sqlem7  25561  2sqblem  25568  chebbnd1lem1  25570  znsqcld  30058  xrsmulgzz  30222  ressmulgnn0  30228  nexple  30615  eulerpartlemsv2  30964  eulerpartlemv  30970  eulerpartlemb  30974  eulerpartlemf  30976  eulerpartlemgvv  30982  eulerpartlemgh  30984  fz0n  32157  bccolsum  32166  nn0prpw  32855  negn0nposznnd  38056  fzsplit1nn0  38160  pell1qrgaplem  38280  monotoddzzfi  38349  jm2.22  38404  jm2.23  38405  rmydioph  38423  expdioph  38432  rp-isfinite6  38704  relexpss1d  38837  relexpmulg  38842  iunrelexpmin2  38844  relexp0a  38848  relexpxpmin  38849  relexpaddss  38850  wallispilem3  41077  etransclem24  41268  pwdif  42330  lighneallem3  42353  lighneallem4  42356  nn0o1gt2ALTV  42434  nn0oALTV  42436  ztprmneprm  42971  blennn0elnn  43217  blen1b  43228  nn0sumshdiglem1  43261