Theorem elnn0 9367

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 9366	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2296	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 3345	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 8136	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 3700	. . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0)
6	5	orbi2i 767	. 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
7	2, 3, 6	3bitri 206	1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

Syntax hints:   ↔ wb 105   ∨ wo 713   = wceq 1395   ∈ wcel 2200   ∪ cun 3195  {csn 3666  0cc0 7995  ℕcn 9106  ℕ₀cn0 9365

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-1cn 8088  ax-icn 8090  ax-addcl 8091  ax-mulcl 8093  ax-i2m1 8100

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-n0 9366

This theorem is referenced by:  0nn0  9380  nn0ge0  9390  nnnn0addcl  9395  nnm1nn0  9406  elnnnn0b  9409  elnn0z  9455  elznn0nn  9456  elznn0  9457  elznn  9458  nn0ind-raph  9560  nn0ledivnn  9959  expp1  10763  expnegap0  10764  expcllem  10767  nn0ltexp2  10926  facp1  10947  faclbnd  10958  faclbnd3  10960  bcn1  10975  bcval5  10980  hashnncl  11012  fz1f1o  11881  arisum  12004  arisum2  12005  fprodfac  12121  ef0lem  12166  nn0enne  12408  nn0o1gt2  12411  dfgcd2  12530  mulgcd  12532  eucalgf  12572  eucalginv  12573  prmdvdsexpr  12667  rpexp1i  12671  nn0gcdsq  12717  odzdvds  12763  pceq0  12840  fldivp1  12866  pockthg  12875  1arith  12885  4sqlem17  12925  4sqlem19  12927  mulgnn0gsum  13660  mulgnn0p1  13665  mulgnn0subcl  13667  mulgneg  13672  mulgnn0z  13681  mulgnn0dir  13684  mulgnn0ass  13690  submmulg  13698  znf1o  14609  dvexp2  15380  dvply1  15433  lgsdir  15708  lgsabs1  15712  lgseisenlem1  15743  2sqlem7  15794