Theorem elnn0 8608

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 8607	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2151	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 3130	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 7426	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 3461	. . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0)
6	5	orbi2i 712	. 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
7	2, 3, 6	3bitri 204	1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

Syntax hints:   ↔ wb 103   ∨ wo 662   = wceq 1287   ∈ wcel 1436   ∪ cun 2986  {csn 3431  0cc0 7294  ℕcn 8357  ℕ₀cn0 8606

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-1cn 7382  ax-icn 7384  ax-addcl 7385  ax-mulcl 7387  ax-i2m1 7394

This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617  df-un 2992  df-sn 3437  df-n0 8607

This theorem is referenced by:  0nn0  8621  nn0ge0  8631  nnnn0addcl  8636  nnm1nn0  8647  elnnnn0b  8650  elnn0z  8696  elznn0nn  8697  elznn0  8698  elznn  8699  nn0ind-raph  8796  nn0ledivnn  9170  expp1  9861  expnegap0  9862  expcllem  9865  facp1  10035  faclbnd  10046  faclbnd3  10048  bcn1  10063  ibcval5  10068  hashnncl  10101  fz1f1o  10656  nn0enne  10784  nn0o1gt2  10787  dfgcd2  10885  mulgcd  10887  eucalgf  10919  eucalginv  10920  prmdvdsexpr  11011  rpexp1i  11015  nn0gcdsq  11060