Theorem elnn0 9270

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 9269	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2263	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 3305	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 8039	. . . 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 7898  ℕcn 9009  ℕ₀cn0 9268

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 7991  ax-icn 7993  ax-addcl 7994  ax-mulcl 7996  ax-i2m1 8003

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 9269

This theorem is referenced by:  0nn0  9283  nn0ge0  9293  nnnn0addcl  9298  nnm1nn0  9309  elnnnn0b  9312  elnn0z  9358  elznn0nn  9359  elznn0  9360  elznn  9361  nn0ind-raph  9462  nn0ledivnn  9861  expp1  10657  expnegap0  10658  expcllem  10661  nn0ltexp2  10820  facp1  10841  faclbnd  10852  faclbnd3  10854  bcn1  10869  bcval5  10874  hashnncl  10906  fz1f1o  11559  arisum  11682  arisum2  11683  fprodfac  11799  ef0lem  11844  nn0enne  12086  nn0o1gt2  12089  dfgcd2  12208  mulgcd  12210  eucalgf  12250  eucalginv  12251  prmdvdsexpr  12345  rpexp1i  12349  nn0gcdsq  12395  odzdvds  12441  pceq0  12518  fldivp1  12544  pockthg  12553  1arith  12563  4sqlem17  12603  4sqlem19  12605  mulgnn0gsum  13336  mulgnn0p1  13341  mulgnn0subcl  13343  mulgneg  13348  mulgnn0z  13357  mulgnn0dir  13360  mulgnn0ass  13366  submmulg  13374  znf1o  14285  dvexp2  15056  dvply1  15109  lgsdir  15384  lgsabs1  15388  lgseisenlem1  15419  2sqlem7  15470