Theorem elnn0 9251

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 9250	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2263	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 3304	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 8020	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 3656	. . 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 3622  0cc0 7879  ℕcn 8990  ℕ₀cn0 9249

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 7972  ax-icn 7974  ax-addcl 7975  ax-mulcl 7977  ax-i2m1 7984

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 3628  df-n0 9250

This theorem is referenced by:  0nn0  9264  nn0ge0  9274  nnnn0addcl  9279  nnm1nn0  9290  elnnnn0b  9293  elnn0z  9339  elznn0nn  9340  elznn0  9341  elznn  9342  nn0ind-raph  9443  nn0ledivnn  9842  expp1  10638  expnegap0  10639  expcllem  10642  nn0ltexp2  10801  facp1  10822  faclbnd  10833  faclbnd3  10835  bcn1  10850  bcval5  10855  hashnncl  10887  fz1f1o  11540  arisum  11663  arisum2  11664  fprodfac  11780  ef0lem  11825  nn0enne  12067  nn0o1gt2  12070  dfgcd2  12181  mulgcd  12183  eucalgf  12223  eucalginv  12224  prmdvdsexpr  12318  rpexp1i  12322  nn0gcdsq  12368  odzdvds  12414  pceq0  12491  fldivp1  12517  pockthg  12526  1arith  12536  4sqlem17  12576  4sqlem19  12578  mulgnn0gsum  13258  mulgnn0p1  13263  mulgnn0subcl  13265  mulgneg  13270  mulgnn0z  13279  mulgnn0dir  13282  mulgnn0ass  13288  submmulg  13296  znf1o  14207  dvexp2  14948  dvply1  15001  lgsdir  15276  lgsabs1  15280  lgseisenlem1  15311  2sqlem7  15362