Theorem elnn0 9245

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 9244	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2260	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 3301	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 8015	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 3653	. . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0)
6	5	orbi2i 763	. 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
7	2, 3, 6	3bitri 206	1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

Syntax hints:   ↔ wb 105   ∨ wo 709   = wceq 1364   ∈ wcel 2164   ∪ cun 3152  {csn 3619  0cc0 7874  ℕcn 8984  ℕ₀cn0 9243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-1cn 7967  ax-icn 7969  ax-addcl 7970  ax-mulcl 7972  ax-i2m1 7979

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3158  df-sn 3625  df-n0 9244

This theorem is referenced by:  0nn0  9258  nn0ge0  9268  nnnn0addcl  9273  nnm1nn0  9284  elnnnn0b  9287  elnn0z  9333  elznn0nn  9334  elznn0  9335  elznn  9336  nn0ind-raph  9437  nn0ledivnn  9836  expp1  10620  expnegap0  10621  expcllem  10624  nn0ltexp2  10783  facp1  10804  faclbnd  10815  faclbnd3  10817  bcn1  10832  bcval5  10837  hashnncl  10869  fz1f1o  11521  arisum  11644  arisum2  11645  fprodfac  11761  ef0lem  11806  nn0enne  12046  nn0o1gt2  12049  dfgcd2  12154  mulgcd  12156  eucalgf  12196  eucalginv  12197  prmdvdsexpr  12291  rpexp1i  12295  nn0gcdsq  12341  odzdvds  12386  pceq0  12463  fldivp1  12489  pockthg  12498  1arith  12508  4sqlem17  12548  4sqlem19  12550  mulgnn0gsum  13201  mulgnn0p1  13206  mulgnn0subcl  13208  mulgneg  13213  mulgnn0z  13222  mulgnn0dir  13225  mulgnn0ass  13231  submmulg  13239  znf1o  14150  dvexp2  14891  dvply1  14943  lgsdir  15192  lgsabs1  15196  lgseisenlem1  15227  2sqlem7  15278