Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > elnn0 | GIF version |
Description: Nonnegative integers expressed in terms of naturals and zero. (Contributed by Raph Levien, 10-Dec-2002.) |
Ref | Expression |
---|---|
elnn0 | ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-n0 8978 | . . 3 ⊢ ℕ0 = (ℕ ∪ {0}) | |
2 | 1 | eleq2i 2206 | . 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0})) |
3 | elun 3217 | . 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0})) | |
4 | c0ex 7760 | . . . 4 ⊢ 0 ∈ V | |
5 | 4 | elsn2 3559 | . . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0) |
6 | 5 | orbi2i 751 | . 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0)) |
7 | 2, 3, 6 | 3bitri 205 | 1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0)) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ∨ wo 697 = wceq 1331 ∈ wcel 1480 ∪ cun 3069 {csn 3527 0cc0 7620 ℕcn 8720 ℕ0cn0 8977 |
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 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 ax-1cn 7713 ax-icn 7715 ax-addcl 7716 ax-mulcl 7718 ax-i2m1 7725 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-v 2688 df-un 3075 df-sn 3533 df-n0 8978 |
This theorem is referenced by: 0nn0 8992 nn0ge0 9002 nnnn0addcl 9007 nnm1nn0 9018 elnnnn0b 9021 elnn0z 9067 elznn0nn 9068 elznn0 9069 elznn 9070 nn0ind-raph 9168 nn0ledivnn 9554 expp1 10300 expnegap0 10301 expcllem 10304 facp1 10476 faclbnd 10487 faclbnd3 10489 bcn1 10504 bcval5 10509 hashnncl 10542 fz1f1o 11144 arisum 11267 arisum2 11268 ef0lem 11366 nn0enne 11599 nn0o1gt2 11602 dfgcd2 11702 mulgcd 11704 eucalgf 11736 eucalginv 11737 prmdvdsexpr 11828 rpexp1i 11832 nn0gcdsq 11878 dvexp2 12845 |
Copyright terms: Public domain | W3C validator |