Theorem elnn0 9317

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 9316	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2273	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 3318	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 8086	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 3672	. . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0)
6	5	orbi2i 764	. 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
7	2, 3, 6	3bitri 206	1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

Syntax hints:   ↔ wb 105   ∨ wo 710   = wceq 1373   ∈ wcel 2177   ∪ cun 3168  {csn 3638  0cc0 7945  ℕcn 9056  ℕ₀cn0 9315

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-1cn 8038  ax-icn 8040  ax-addcl 8041  ax-mulcl 8043  ax-i2m1 8050

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-un 3174  df-sn 3644  df-n0 9316

This theorem is referenced by:  0nn0  9330  nn0ge0  9340  nnnn0addcl  9345  nnm1nn0  9356  elnnnn0b  9359  elnn0z  9405  elznn0nn  9406  elznn0  9407  elznn  9408  nn0ind-raph  9510  nn0ledivnn  9909  expp1  10713  expnegap0  10714  expcllem  10717  nn0ltexp2  10876  facp1  10897  faclbnd  10908  faclbnd3  10910  bcn1  10925  bcval5  10930  hashnncl  10962  fz1f1o  11761  arisum  11884  arisum2  11885  fprodfac  12001  ef0lem  12046  nn0enne  12288  nn0o1gt2  12291  dfgcd2  12410  mulgcd  12412  eucalgf  12452  eucalginv  12453  prmdvdsexpr  12547  rpexp1i  12551  nn0gcdsq  12597  odzdvds  12643  pceq0  12720  fldivp1  12746  pockthg  12755  1arith  12765  4sqlem17  12805  4sqlem19  12807  mulgnn0gsum  13539  mulgnn0p1  13544  mulgnn0subcl  13546  mulgneg  13551  mulgnn0z  13560  mulgnn0dir  13563  mulgnn0ass  13569  submmulg  13577  znf1o  14488  dvexp2  15259  dvply1  15312  lgsdir  15587  lgsabs1  15591  lgseisenlem1  15622  2sqlem7  15673