Theorem elnn0 9268

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 9267	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2263	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 3305	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 8037	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 3657	. . 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 2167   ∪ cun 3155  {csn 3623  0cc0 7896  ℕcn 9007  ℕ₀cn0 9266

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-1cn 7989  ax-icn 7991  ax-addcl 7992  ax-mulcl 7994  ax-i2m1 8001

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-sn 3629  df-n0 9267

This theorem is referenced by:  0nn0  9281  nn0ge0  9291  nnnn0addcl  9296  nnm1nn0  9307  elnnnn0b  9310  elnn0z  9356  elznn0nn  9357  elznn0  9358  elznn  9359  nn0ind-raph  9460  nn0ledivnn  9859  expp1  10655  expnegap0  10656  expcllem  10659  nn0ltexp2  10818  facp1  10839  faclbnd  10850  faclbnd3  10852  bcn1  10867  bcval5  10872  hashnncl  10904  fz1f1o  11557  arisum  11680  arisum2  11681  fprodfac  11797  ef0lem  11842  nn0enne  12084  nn0o1gt2  12087  dfgcd2  12206  mulgcd  12208  eucalgf  12248  eucalginv  12249  prmdvdsexpr  12343  rpexp1i  12347  nn0gcdsq  12393  odzdvds  12439  pceq0  12516  fldivp1  12542  pockthg  12551  1arith  12561  4sqlem17  12601  4sqlem19  12603  mulgnn0gsum  13334  mulgnn0p1  13339  mulgnn0subcl  13341  mulgneg  13346  mulgnn0z  13355  mulgnn0dir  13358  mulgnn0ass  13364  submmulg  13372  znf1o  14283  dvexp2  15032  dvply1  15085  lgsdir  15360  lgsabs1  15364  lgseisenlem1  15395  2sqlem7  15446