Theorem elnn0 12165

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 12164	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2830	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 4079	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 10900	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 4597	. . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0)
6	5	orbi2i 909	. 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
7	2, 3, 6	3bitri 296	1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

Syntax hints:   ↔ wb 205   ∨ wo 843   = wceq 1539   ∈ wcel 2108   ∪ cun 3881  {csn 4558  0cc0 10802  ℕcn 11903  ℕ₀cn0 12163

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-mulcl 10864  ax-i2m1 10870

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-sn 4559  df-n0 12164

This theorem is referenced by:  0nn0  12178  nn0ge0  12188  nnnn0addcl  12193  nnm1nn0  12204  elnnnn0b  12207  nn0sub  12213  elnn0z  12262  elznn0nn  12263  elznn0  12264  elznn  12265  nn0lt10b  12312  nn0ind-raph  12350  nn0ledivnn  12772  expp1  13717  expneg  13718  expcllem  13721  znsqcld  13808  facp1  13920  faclbnd  13932  faclbnd3  13934  faclbnd4lem1  13935  faclbnd4lem3  13937  faclbnd4  13939  bcn1  13955  bcval5  13960  hashv01gt1  13987  hashnncl  14009  seqcoll2  14107  relexpsucl  14670  relexpsucr  14671  relexpcnv  14674  relexprelg  14677  relexpdmg  14681  relexprng  14685  relexpfld  14688  relexpaddg  14692  fz1f1o  15350  arisum  15500  arisum2  15501  pwdif  15508  geomulcvg  15516  fprodfac  15611  ef0lem  15716  nn0enne  16014  nn0o1gt2  16018  bezoutlem3  16177  dfgcd2  16182  mulgcd  16184  eucalgf  16216  eucalginv  16217  eucalglt  16218  prmdvdsexpr  16350  rpexp1i  16356  nn0gcdsq  16384  odzdvds  16424  pceq0  16500  fldivp1  16526  pockthg  16535  1arith  16556  4sqlem17  16590  4sqlem19  16592  vdwmc2  16608  vdwlem13  16622  0ram  16649  ram0  16651  ramz  16654  ramcl  16658  mulgnn0gsum  18625  mulgnn0p1  18630  mulgnn0subcl  18632  mulgneg  18637  mulgnn0z  18645  mulgnn0dir  18648  mulgnn0ass  18654  submmulg  18662  odcl  19059  mndodcongi  19066  oddvdsnn0  19067  odnncl  19068  oddvds  19070  dfod2  19086  odcl2  19087  gexcl  19100  gexdvds  19104  gexnnod  19108  sylow1lem1  19118  mulgnn0di  19342  torsubg  19370  ablfac1eu  19591  gzrngunitlem  20575  zringlpirlem3  20598  prmirredlem  20606  prmirred  20608  znf1o  20671  evlslem3  21200  dscmet  23634  dvexp2  25023  tdeglem4  25129  tdeglem4OLD  25130  dgrnznn  25313  coefv0  25314  dgreq0  25331  dgrcolem2  25340  dvply1  25349  aaliou2  25405  radcnv0  25480  logfac  25661  logtayl  25720  cxpexp  25728  birthdaylem2  26007  harmonicbnd3  26062  sqf11  26193  ppiltx  26231  sqff1o  26236  lgsdir  26385  lgsabs1  26389  lgseisenlem1  26428  2sqlem7  26477  2sqblem  26484  2sqnn  26492  chebbnd1lem1  26522  xrsmulgzz  31189  ressmulgnn0  31195  nexple  31877  eulerpartlemsv2  32225  eulerpartlemv  32231  eulerpartlemb  32235  eulerpartlemf  32237  eulerpartlemgvv  32243  eulerpartlemgh  32245  fz0n  33602  bccolsum  33611  nn0prpw  34439  aks4d1p1  40012  sticksstones13  40043  fsuppind  40202  negn0nposznnd  40231  nn0rppwr  40254  nn0expgcd  40256  dvdsexpnn0  40262  fzsplit1nn0  40492  pell1qrgaplem  40611  monotoddzzfi  40680  jm2.22  40733  jm2.23  40734  rmydioph  40752  expdioph  40761  rp-isfinite6  41023  relexpss1d  41202  relexpmulg  41207  iunrelexpmin2  41209  relexp0a  41213  relexpxpmin  41214  relexpaddss  41215  wallispilem3  43498  etransclem24  43689  lighneallem3  44947  lighneallem4  44950  nn0o1gt2ALTV  45034  nn0oALTV  45036  ztprmneprm  45571  blennn0elnn  45811  blen1b  45822  nn0sumshdiglem1  45855