Theorem elnn0 8883

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 8882	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2181	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 3183	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 7684	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 3525	. . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0)
6	5	orbi2i 734	. 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
7	2, 3, 6	3bitri 205	1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

Syntax hints:   ↔ wb 104   ∨ wo 680   = wceq 1314   ∈ wcel 1463   ∪ cun 3035  {csn 3493  0cc0 7547  ℕcn 8630  ℕ₀cn0 8881

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-1cn 7638  ax-icn 7640  ax-addcl 7641  ax-mulcl 7643  ax-i2m1 7650

This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2244  df-v 2659  df-un 3041  df-sn 3499  df-n0 8882

This theorem is referenced by:  0nn0  8896  nn0ge0  8906  nnnn0addcl  8911  nnm1nn0  8922  elnnnn0b  8925  elnn0z  8971  elznn0nn  8972  elznn0  8973  elznn  8974  nn0ind-raph  9072  nn0ledivnn  9447  expp1  10193  expnegap0  10194  expcllem  10197  facp1  10369  faclbnd  10380  faclbnd3  10382  bcn1  10397  bcval5  10402  hashnncl  10435  fz1f1o  11036  arisum  11159  arisum2  11160  ef0lem  11217  nn0enne  11447  nn0o1gt2  11450  dfgcd2  11548  mulgcd  11550  eucalgf  11582  eucalginv  11583  prmdvdsexpr  11674  rpexp1i  11678  nn0gcdsq  11723