Theorem elnn0 9279

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 9278	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2271	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 3313	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 8048	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 3666	. . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0)
6	5	orbi2i 763	. 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
7	2, 3, 6	3bitri 206	1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

Syntax hints:   ↔ wb 105   ∨ wo 709   = wceq 1372   ∈ wcel 2175   ∪ cun 3163  {csn 3632  0cc0 7907  ℕcn 9018  ℕ₀cn0 9277

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186  ax-1cn 8000  ax-icn 8002  ax-addcl 8003  ax-mulcl 8005  ax-i2m1 8012

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-un 3169  df-sn 3638  df-n0 9278

This theorem is referenced by:  0nn0  9292  nn0ge0  9302  nnnn0addcl  9307  nnm1nn0  9318  elnnnn0b  9321  elnn0z  9367  elznn0nn  9368  elznn0  9369  elznn  9370  nn0ind-raph  9472  nn0ledivnn  9871  expp1  10672  expnegap0  10673  expcllem  10676  nn0ltexp2  10835  facp1  10856  faclbnd  10867  faclbnd3  10869  bcn1  10884  bcval5  10889  hashnncl  10921  fz1f1o  11605  arisum  11728  arisum2  11729  fprodfac  11845  ef0lem  11890  nn0enne  12132  nn0o1gt2  12135  dfgcd2  12254  mulgcd  12256  eucalgf  12296  eucalginv  12297  prmdvdsexpr  12391  rpexp1i  12395  nn0gcdsq  12441  odzdvds  12487  pceq0  12564  fldivp1  12590  pockthg  12599  1arith  12609  4sqlem17  12649  4sqlem19  12651  mulgnn0gsum  13382  mulgnn0p1  13387  mulgnn0subcl  13389  mulgneg  13394  mulgnn0z  13403  mulgnn0dir  13406  mulgnn0ass  13412  submmulg  13420  znf1o  14331  dvexp2  15102  dvply1  15155  lgsdir  15430  lgsabs1  15434  lgseisenlem1  15465  2sqlem7  15516