Theorem elnn0 9242

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 9241	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2260	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 3300	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 8013	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 3652	. . 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 3151  {csn 3618  0cc0 7872  ℕcn 8982  ℕ₀cn0 9240

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 7965  ax-icn 7967  ax-addcl 7968  ax-mulcl 7970  ax-i2m1 7977

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 3157  df-sn 3624  df-n0 9241

This theorem is referenced by:  0nn0  9255  nn0ge0  9265  nnnn0addcl  9270  nnm1nn0  9281  elnnnn0b  9284  elnn0z  9330  elznn0nn  9331  elznn0  9332  elznn  9333  nn0ind-raph  9434  nn0ledivnn  9833  expp1  10617  expnegap0  10618  expcllem  10621  nn0ltexp2  10780  facp1  10801  faclbnd  10812  faclbnd3  10814  bcn1  10829  bcval5  10834  hashnncl  10866  fz1f1o  11518  arisum  11641  arisum2  11642  fprodfac  11758  ef0lem  11803  nn0enne  12043  nn0o1gt2  12046  dfgcd2  12151  mulgcd  12153  eucalgf  12193  eucalginv  12194  prmdvdsexpr  12288  rpexp1i  12292  nn0gcdsq  12338  odzdvds  12383  pceq0  12460  fldivp1  12486  pockthg  12495  1arith  12505  4sqlem17  12545  4sqlem19  12547  mulgnn0gsum  13198  mulgnn0p1  13203  mulgnn0subcl  13205  mulgneg  13210  mulgnn0z  13219  mulgnn0dir  13222  mulgnn0ass  13228  submmulg  13236  znf1o  14139  dvexp2  14861  lgsdir  15151  lgsabs1  15155  lgseisenlem1  15186  2sqlem7  15208