Theorem elnn0 9296

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 9295	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2271	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 3313	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 8065	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 3666	. . 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 1372   ∈ wcel 2175   ∪ cun 3163  {csn 3632  0cc0 7924  ℕcn 9035  ℕ₀cn0 9294

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186  ax-1cn 8017  ax-icn 8019  ax-addcl 8020  ax-mulcl 8022  ax-i2m1 8029

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-un 3169  df-sn 3638  df-n0 9295

This theorem is referenced by:  0nn0  9309  nn0ge0  9319  nnnn0addcl  9324  nnm1nn0  9335  elnnnn0b  9338  elnn0z  9384  elznn0nn  9385  elznn0  9386  elznn  9387  nn0ind-raph  9489  nn0ledivnn  9888  expp1  10689  expnegap0  10690  expcllem  10693  nn0ltexp2  10852  facp1  10873  faclbnd  10884  faclbnd3  10886  bcn1  10901  bcval5  10906  hashnncl  10938  fz1f1o  11628  arisum  11751  arisum2  11752  fprodfac  11868  ef0lem  11913  nn0enne  12155  nn0o1gt2  12158  dfgcd2  12277  mulgcd  12279  eucalgf  12319  eucalginv  12320  prmdvdsexpr  12414  rpexp1i  12418  nn0gcdsq  12464  odzdvds  12510  pceq0  12587  fldivp1  12613  pockthg  12622  1arith  12632  4sqlem17  12672  4sqlem19  12674  mulgnn0gsum  13406  mulgnn0p1  13411  mulgnn0subcl  13413  mulgneg  13418  mulgnn0z  13427  mulgnn0dir  13430  mulgnn0ass  13436  submmulg  13444  znf1o  14355  dvexp2  15126  dvply1  15179  lgsdir  15454  lgsabs1  15458  lgseisenlem1  15489  2sqlem7  15540