Theorem elnn0 9576

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 9575	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2305	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 3370	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 8326	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 3743	. . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0)
6	5	orbi2i 774	. 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
7	2, 3, 6	3bitri 206	1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

This proof depends on syntax axioms:   ↔ wb 105   ∨ wo 720   = wceq 1402   ∈ wcel 2209   ∪ cun 3218  {csn 3709  0cc0 8185  ℕcn 9313  ℕ₀cn0 9574

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-1cn 8278  ax-icn 8280  ax-addcl 8281  ax-mulcl 8283  ax-i2m1 8290

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3715  df-n0 9575

This theorem is used by:  0nn0  9589  nn0ge0  9599  nnnn0addcl  9604  nnm1nn0  9615  elnnnn0b  9618  elnn0z  9666  elznn0nn  9667  elznn0  9668  elznn  9669  nn0ind-raph  9773  nn0ledivnn  10184  expp1  11003  expnegap0  11004  expcllem  11007  nn0ltexp2  11168  facp1  11189  faclbnd  11200  faclbnd3  11202  bcn1  11217  bcval5  11222  hashnncl  11255  fz1f1o  12165  arisum  12289  arisum2  12290  fprodfac  12406  ef0lem  12451  nn0enne  12693  nn0o1gt2  12696  dfgcd2  12815  mulgcd  12817  eucalgf  12857  eucalginv  12858  prmdvdsexpr  12953  rpexp1i  12957  nn0gcdsq  13004  odzdvds  13052  pceq0  13129  fldivp1  13155  pockthg  13164  1arith  13174  4sqlem17  13214  4sqlem19  13216  mulgnn0gzsum  13989  mulgnn0p1  13994  mulgnn0subcl  13996  mulgneg  14001  mulgnn0z  14010  mulgnn0dir  14013  mulgnn0ass  14019  submmulg  14027  gsumvalfi  14241  znf1o  15094  dvexp2  15955  dvply1  16008  logfac  16143  birthdaylem2  16243  ppiqltx  16298  lgsdir  16376  lgsabs1  16380  lgseisenlem1  16411  2sqlem7  16462  clwwlknnn  16875