Theorem elnn0 11900

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 11899	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2904	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 4125	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 10635	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 4604	. . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0)
6	5	orbi2i 909	. 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
7	2, 3, 6	3bitri 299	1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

Syntax hints:   ↔ wb 208   ∨ wo 843   = wceq 1537   ∈ wcel 2114   ∪ cun 3934  {csn 4567  0cc0 10537  ℕcn 11638  ℕ₀cn0 11898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-mulcl 10599  ax-i2m1 10605

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3941  df-sn 4568  df-n0 11899

This theorem is referenced by:  0nn0  11913  nn0ge0  11923  nnnn0addcl  11928  nnm1nn0  11939  elnnnn0b  11942  nn0sub  11948  elnn0z  11995  elznn0nn  11996  elznn0  11997  elznn  11998  nn0lt10b  12045  nn0ind-raph  12083  nn0ledivnn  12503  expp1  13437  expneg  13438  expcllem  13441  znsqcld  13527  facp1  13639  faclbnd  13651  faclbnd3  13653  faclbnd4lem1  13654  faclbnd4lem3  13656  faclbnd4  13658  bcn1  13674  bcval5  13679  hashv01gt1  13706  hashnncl  13728  seqcoll2  13824  relexpsucr  14388  relexpsucl  14392  relexpcnv  14394  relexprelg  14397  relexpdmg  14401  relexprng  14405  relexpfld  14408  relexpaddg  14412  fz1f1o  15067  arisum  15215  arisum2  15216  pwdif  15223  geomulcvg  15232  fprodfac  15327  ef0lem  15432  nn0enne  15728  nn0o1gt2  15732  bezoutlem3  15889  dfgcd2  15894  mulgcd  15896  eucalgf  15927  eucalginv  15928  eucalglt  15929  prmdvdsexpr  16061  rpexp1i  16065  nn0gcdsq  16092  odzdvds  16132  pceq0  16207  fldivp1  16233  pockthg  16242  1arith  16263  4sqlem17  16297  4sqlem19  16299  vdwmc2  16315  vdwlem13  16329  0ram  16356  ram0  16358  ramz  16361  ramcl  16365  mulgnn0gsum  18234  mulgnn0p1  18239  mulgnn0subcl  18241  mulgneg  18246  mulgnn0z  18254  mulgnn0dir  18257  mulgnn0ass  18263  submmulg  18271  odcl  18664  mndodcongi  18671  oddvdsnn0  18672  odnncl  18673  oddvds  18675  dfod2  18691  odcl2  18692  gexcl  18705  gexdvds  18709  gexnnod  18713  sylow1lem1  18723  mulgnn0di  18946  torsubg  18974  ablfac1eu  19195  evlslem3  20293  gzrngunitlem  20610  zringlpirlem3  20633  prmirredlem  20640  prmirred  20642  znf1o  20698  dscmet  23182  dvexp2  24551  tdeglem4  24654  dgrnznn  24837  coefv0  24838  dgreq0  24855  dgrcolem2  24864  dvply1  24873  aaliou2  24929  radcnv0  25004  logfac  25184  logtayl  25243  cxpexp  25251  birthdaylem2  25530  harmonicbnd3  25585  sqf11  25716  ppiltx  25754  sqff1o  25759  lgsdir  25908  lgsabs1  25912  lgseisenlem1  25951  2sqlem7  26000  2sqblem  26007  2sqnn  26015  chebbnd1lem1  26045  xrsmulgzz  30665  ressmulgnn0  30671  nexple  31268  eulerpartlemsv2  31616  eulerpartlemv  31622  eulerpartlemb  31626  eulerpartlemf  31628  eulerpartlemgvv  31634  eulerpartlemgh  31636  fz0n  32962  bccolsum  32971  nn0prpw  33671  negn0nposznnd  39217  nn0rppwr  39231  nn0expgcd  39233  fzsplit1nn0  39400  pell1qrgaplem  39519  monotoddzzfi  39588  jm2.22  39641  jm2.23  39642  rmydioph  39660  expdioph  39669  rp-isfinite6  39933  relexpss1d  40099  relexpmulg  40104  iunrelexpmin2  40106  relexp0a  40110  relexpxpmin  40111  relexpaddss  40112  wallispilem3  42401  etransclem24  42592  lighneallem3  43821  lighneallem4  43824  nn0o1gt2ALTV  43908  nn0oALTV  43910  ztprmneprm  44444  blennn0elnn  44686  blen1b  44697  nn0sumshdiglem1  44730