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 8946 | . . 3 ⊢ ℕ0 = (ℕ ∪ {0}) | |
2 | 1 | eleq2i 2184 | . 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0})) |
3 | elun 3187 | . 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0})) | |
4 | c0ex 7728 | . . . 4 ⊢ 0 ∈ V | |
5 | 4 | elsn2 3529 | . . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0) |
6 | 5 | orbi2i 736 | . 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0)) |
7 | 2, 3, 6 | 3bitri 205 | 1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0)) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ∨ wo 682 = wceq 1316 ∈ wcel 1465 ∪ cun 3039 {csn 3497 0cc0 7588 ℕcn 8688 ℕ0cn0 8945 |
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 683 ax-5 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-10 1468 ax-11 1469 ax-i12 1470 ax-bndl 1471 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 ax-1cn 7681 ax-icn 7683 ax-addcl 7684 ax-mulcl 7686 ax-i2m1 7693 |
This theorem depends on definitions: df-bi 116 df-tru 1319 df-nf 1422 df-sb 1721 df-clab 2104 df-cleq 2110 df-clel 2113 df-nfc 2247 df-v 2662 df-un 3045 df-sn 3503 df-n0 8946 |
This theorem is referenced by: 0nn0 8960 nn0ge0 8970 nnnn0addcl 8975 nnm1nn0 8986 elnnnn0b 8989 elnn0z 9035 elznn0nn 9036 elznn0 9037 elznn 9038 nn0ind-raph 9136 nn0ledivnn 9522 expp1 10268 expnegap0 10269 expcllem 10272 facp1 10444 faclbnd 10455 faclbnd3 10457 bcn1 10472 bcval5 10477 hashnncl 10510 fz1f1o 11112 arisum 11235 arisum2 11236 ef0lem 11293 nn0enne 11526 nn0o1gt2 11529 dfgcd2 11629 mulgcd 11631 eucalgf 11663 eucalginv 11664 prmdvdsexpr 11755 rpexp1i 11759 nn0gcdsq 11805 dvexp2 12772 |
Copyright terms: Public domain | W3C validator |