Theorem elnn0 9137

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 9136	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2237	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 3268	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 7914	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 3617	. . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0)
6	5	orbi2i 757	. 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
7	2, 3, 6	3bitri 205	1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

Syntax hints:   ↔ wb 104   ∨ wo 703   = wceq 1348   ∈ wcel 2141   ∪ cun 3119  {csn 3583  0cc0 7774  ℕcn 8878  ℕ₀cn0 9135

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-1cn 7867  ax-icn 7869  ax-addcl 7870  ax-mulcl 7872  ax-i2m1 7879

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-sn 3589  df-n0 9136

This theorem is referenced by:  0nn0  9150  nn0ge0  9160  nnnn0addcl  9165  nnm1nn0  9176  elnnnn0b  9179  elnn0z  9225  elznn0nn  9226  elznn0  9227  elznn  9228  nn0ind-raph  9329  nn0ledivnn  9724  expp1  10483  expnegap0  10484  expcllem  10487  nn0ltexp2  10644  facp1  10664  faclbnd  10675  faclbnd3  10677  bcn1  10692  bcval5  10697  hashnncl  10730  fz1f1o  11338  arisum  11461  arisum2  11462  fprodfac  11578  ef0lem  11623  nn0enne  11861  nn0o1gt2  11864  dfgcd2  11969  mulgcd  11971  eucalgf  12009  eucalginv  12010  prmdvdsexpr  12104  rpexp1i  12108  nn0gcdsq  12154  odzdvds  12199  pceq0  12275  fldivp1  12300  pockthg  12309  1arith  12319  dvexp2  13470  lgsdir  13730  lgsabs1  13734  2sqlem7  13751