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  10808  expnegap0  10809  expcllem  10812  nn0ltexp2  10971  facp1  10992  faclbnd  11003  faclbnd3  11005  bcn1  11020  bcval5  11025  hashnncl  11057  fz1f1o  11936  arisum  12060  arisum2  12061  fprodfac  12177  ef0lem  12222  nn0enne  12464  nn0o1gt2  12467  dfgcd2  12586  mulgcd  12588  eucalgf  12628  eucalginv  12629  prmdvdsexpr  12723  rpexp1i  12727  nn0gcdsq  12773  odzdvds  12819  pceq0  12896  fldivp1  12922  pockthg  12931  1arith  12941  4sqlem17  12981  4sqlem19  12983  mulgnn0gsum  13716  mulgnn0p1  13721  mulgnn0subcl  13723  mulgneg  13728  mulgnn0z  13737  mulgnn0dir  13740  mulgnn0ass  13746  submmulg  13754  znf1o  14667  dvexp2  15438  dvply1  15491  lgsdir  15766  lgsabs1  15770  lgseisenlem1  15801  2sqlem7  15852  clwwlknnn  16265  gfsumval  16683