Theorem elnn0 9403

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 9402	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2298	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 3348	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 8172	. . . 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 8031  ℕcn 9142  ℕ₀cn0 9401

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 8124  ax-icn 8126  ax-addcl 8127  ax-mulcl 8129  ax-i2m1 8136

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 9402

This theorem is referenced by:  0nn0  9416  nn0ge0  9426  nnnn0addcl  9431  nnm1nn0  9442  elnnnn0b  9445  elnn0z  9491  elznn0nn  9492  elznn0  9493  elznn  9494  nn0ind-raph  9596  nn0ledivnn  10001  expp1  10807  expnegap0  10808  expcllem  10811  nn0ltexp2  10970  facp1  10991  faclbnd  11002  faclbnd3  11004  bcn1  11019  bcval5  11024  hashnncl  11056  fz1f1o  11935  arisum  12058  arisum2  12059  fprodfac  12175  ef0lem  12220  nn0enne  12462  nn0o1gt2  12465  dfgcd2  12584  mulgcd  12586  eucalgf  12626  eucalginv  12627  prmdvdsexpr  12721  rpexp1i  12725  nn0gcdsq  12771  odzdvds  12817  pceq0  12894  fldivp1  12920  pockthg  12929  1arith  12939  4sqlem17  12979  4sqlem19  12981  mulgnn0gsum  13714  mulgnn0p1  13719  mulgnn0subcl  13721  mulgneg  13726  mulgnn0z  13735  mulgnn0dir  13738  mulgnn0ass  13744  submmulg  13752  znf1o  14664  dvexp2  15435  dvply1  15488  lgsdir  15763  lgsabs1  15767  lgseisenlem1  15798  2sqlem7  15849  clwwlknnn  16262  gfsumval  16680