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  9668  elznn0nn  9669  elznn0  9670  elznn  9671  nn0ind-raph  9774  nn0ledivnn  10185  expp1  11004  expnegap0  11005  expcllem  11008  nn0ltexp2  11169  facp1  11190  faclbnd  11201  faclbnd3  11203  bcn1  11218  bcval5  11223  hashnncl  11256  fz1f1o  12166  arisum  12290  arisum2  12291  fprodfac  12407  ef0lem  12452  nn0enne  12694  nn0o1gt2  12697  dfgcd2  12816  mulgcd  12818  eucalgf  12858  eucalginv  12859  prmdvdsexpr  12954  rpexp1i  12958  nn0gcdsq  13005  odzdvds  13053  pceq0  13130  fldivp1  13156  pockthg  13165  1arith  13175  4sqlem17  13215  4sqlem19  13217  mulgnn0gzsum  13990  mulgnn0p1  13995  mulgnn0subcl  13997  mulgneg  14002  mulgnn0z  14011  mulgnn0dir  14014  mulgnn0ass  14020  submmulg  14028  gsumvalfi  14242  znf1o  15095  dvexp2  15938  dvply1  15991  logfac  16126  birthdaylem2  16226  ppiqltx  16281  lgsdir  16359  lgsabs1  16363  lgseisenlem1  16394  2sqlem7  16445  clwwlknnn  16858