Theorem elnn0 9404

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 9403	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2298	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 3348	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 8173	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 3703	. . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0)
6	5	orbi2i 769	. 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
7	2, 3, 6	3bitri 206	1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

Syntax hints:   ↔ wb 105   ∨ wo 715   = wceq 1397   ∈ wcel 2202   ∪ cun 3198  {csn 3669  0cc0 8032  ℕcn 9143  ℕ₀cn0 9402

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-1cn 8125  ax-icn 8127  ax-addcl 8128  ax-mulcl 8130  ax-i2m1 8137

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-sn 3675  df-n0 9403

This theorem is referenced by:  0nn0  9417  nn0ge0  9427  nnnn0addcl  9432  nnm1nn0  9443  elnnnn0b  9446  elnn0z  9492  elznn0nn  9493  elznn0  9494  elznn  9495  nn0ind-raph  9597  nn0ledivnn  10002  expp1  10809  expnegap0  10810  expcllem  10813  nn0ltexp2  10972  facp1  10993  faclbnd  11004  faclbnd3  11006  bcn1  11021  bcval5  11026  hashnncl  11058  fz1f1o  11940  arisum  12064  arisum2  12065  fprodfac  12181  ef0lem  12226  nn0enne  12468  nn0o1gt2  12471  dfgcd2  12590  mulgcd  12592  eucalgf  12632  eucalginv  12633  prmdvdsexpr  12727  rpexp1i  12731  nn0gcdsq  12777  odzdvds  12823  pceq0  12900  fldivp1  12926  pockthg  12935  1arith  12945  4sqlem17  12985  4sqlem19  12987  mulgnn0gsum  13720  mulgnn0p1  13725  mulgnn0subcl  13727  mulgneg  13732  mulgnn0z  13741  mulgnn0dir  13744  mulgnn0ass  13750  submmulg  13758  znf1o  14671  dvexp2  15442  dvply1  15495  lgsdir  15770  lgsabs1  15774  lgseisenlem1  15805  2sqlem7  15856  clwwlknnn  16269  gfsumval  16707