Theorem elnn0 9446

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 9445	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2298	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 3350	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 8216	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 3707	. . 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 2202   ∪ cun 3199  {csn 3673  0cc0 8075  ℕcn 9185  ℕ₀cn0 9444

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 2213  ax-1cn 8168  ax-icn 8170  ax-addcl 8171  ax-mulcl 8173  ax-i2m1 8180

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-un 3205  df-sn 3679  df-n0 9445

This theorem is referenced by:  0nn0  9459  nn0ge0  9469  nnnn0addcl  9474  nnm1nn0  9485  elnnnn0b  9488  elnn0z  9536  elznn0nn  9537  elznn0  9538  elznn  9539  nn0ind-raph  9641  nn0ledivnn  10046  expp1  10854  expnegap0  10855  expcllem  10858  nn0ltexp2  11017  facp1  11038  faclbnd  11049  faclbnd3  11051  bcn1  11066  bcval5  11071  hashnncl  11103  fz1f1o  11998  arisum  12122  arisum2  12123  fprodfac  12239  ef0lem  12284  nn0enne  12526  nn0o1gt2  12529  dfgcd2  12648  mulgcd  12650  eucalgf  12690  eucalginv  12691  prmdvdsexpr  12785  rpexp1i  12789  nn0gcdsq  12835  odzdvds  12881  pceq0  12958  fldivp1  12984  pockthg  12993  1arith  13003  4sqlem17  13043  4sqlem19  13045  mulgnn0gsum  13778  mulgnn0p1  13783  mulgnn0subcl  13785  mulgneg  13790  mulgnn0z  13799  mulgnn0dir  13802  mulgnn0ass  13808  submmulg  13816  znf1o  14730  dvexp2  15506  dvply1  15559  lgsdir  15837  lgsabs1  15841  lgseisenlem1  15872  2sqlem7  15923  clwwlknnn  16336  gfsumval  16792