Theorem elnn0 9570

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 9569	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2305	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 3370	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 8321	. . . 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 8180  ℕcn 9307  ℕ₀cn0 9568

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 8273  ax-icn 8275  ax-addcl 8276  ax-mulcl 8278  ax-i2m1 8285

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 9569

This theorem is used by:  0nn0  9583  nn0ge0  9593  nnnn0addcl  9598  nnm1nn0  9609  elnnnn0b  9612  elnn0z  9662  elznn0nn  9663  elznn0  9664  elznn  9665  nn0ind-raph  9768  nn0ledivnn  10179  expp1  10998  expnegap0  10999  expcllem  11002  nn0ltexp2  11163  facp1  11184  faclbnd  11195  faclbnd3  11197  bcn1  11212  bcval5  11217  hashnncl  11250  fz1f1o  12160  arisum  12284  arisum2  12285  fprodfac  12401  ef0lem  12446  nn0enne  12688  nn0o1gt2  12691  dfgcd2  12810  mulgcd  12812  eucalgf  12852  eucalginv  12853  prmdvdsexpr  12948  rpexp1i  12952  nn0gcdsq  12999  odzdvds  13047  pceq0  13124  fldivp1  13150  pockthg  13159  1arith  13169  4sqlem17  13209  4sqlem19  13211  mulgnn0gzsum  13984  mulgnn0p1  13989  mulgnn0subcl  13991  mulgneg  13996  mulgnn0z  14005  mulgnn0dir  14008  mulgnn0ass  14014  submmulg  14022  gsumvalfi  14236  znf1o  15070  dvexp2  15904  dvply1  15957  logfac  16090  birthdaylem2  16187  ppiqltx  16242  lgsdir  16320  lgsabs1  16324  lgseisenlem1  16355  2sqlem7  16406  clwwlknnn  16819