Theorem elnn0 9515

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 9514	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2301	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 3364	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 8284	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 3728	. . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0)
6	5	orbi2i 770	. 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
7	2, 3, 6	3bitri 206	1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

Syntax hints:   ↔ wb 105   ∨ wo 716   = wceq 1398   ∈ wcel 2205   ∪ cun 3212  {csn 3694  0cc0 8143  ℕcn 9254  ℕ₀cn0 9513

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-1cn 8236  ax-icn 8238  ax-addcl 8239  ax-mulcl 8241  ax-i2m1 8248

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3218  df-sn 3700  df-n0 9514

This theorem is referenced by:  0nn0  9528  nn0ge0  9538  nnnn0addcl  9543  nnm1nn0  9554  elnnnn0b  9557  elnn0z  9607  elznn0nn  9608  elznn0  9609  elznn  9610  nn0ind-raph  9713  nn0ledivnn  10118  expp1  10932  expnegap0  10933  expcllem  10936  nn0ltexp2  11096  facp1  11117  faclbnd  11128  faclbnd3  11130  bcn1  11145  bcval5  11150  hashnncl  11183  fz1f1o  12085  arisum  12209  arisum2  12210  fprodfac  12326  ef0lem  12371  nn0enne  12613  nn0o1gt2  12616  dfgcd2  12735  mulgcd  12737  eucalgf  12777  eucalginv  12778  prmdvdsexpr  12872  rpexp1i  12876  nn0gcdsq  12922  odzdvds  12968  pceq0  13045  fldivp1  13071  pockthg  13080  1arith  13090  4sqlem17  13130  4sqlem19  13132  mulgnn0gsum  13881  mulgnn0p1  13886  mulgnn0subcl  13888  mulgneg  13893  mulgnn0z  13902  mulgnn0dir  13905  mulgnn0ass  13911  submmulg  13919  gfsumval  14102  znf1o  14925  dvexp2  15703  dvply1  15756  lgsdir  16034  lgsabs1  16038  lgseisenlem1  16069  2sqlem7  16120  clwwlknnn  16533