![]() |
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 8566 | . . 3 ⊢ ℕ0 = (ℕ ∪ {0}) | |
2 | 1 | eleq2i 2149 | . 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0})) |
3 | elun 3125 | . 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0})) | |
4 | c0ex 7385 | . . . 4 ⊢ 0 ∈ V | |
5 | 4 | elsn2 3452 | . . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0) |
6 | 5 | orbi2i 712 | . 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0)) |
7 | 2, 3, 6 | 3bitri 204 | 1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0)) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 103 ∨ wo 662 = wceq 1285 ∈ wcel 1434 ∪ cun 2982 {csn 3422 0cc0 7253 ℕcn 8316 ℕ0cn0 8565 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 ax-1cn 7341 ax-icn 7343 ax-addcl 7344 ax-mulcl 7346 ax-i2m1 7353 |
This theorem depends on definitions: df-bi 115 df-tru 1288 df-nf 1391 df-sb 1688 df-clab 2070 df-cleq 2076 df-clel 2079 df-nfc 2212 df-v 2614 df-un 2988 df-sn 3428 df-n0 8566 |
This theorem is referenced by: 0nn0 8580 nn0ge0 8590 nnnn0addcl 8595 nnm1nn0 8606 elnnnn0b 8609 elnn0z 8659 elznn0nn 8660 elznn0 8661 elznn 8662 nn0ind-raph 8759 nn0ledivnn 9133 expp1 9799 expnegap0 9800 expcllem 9803 facp1 9973 faclbnd 9984 faclbnd3 9986 bcn1 10001 ibcval5 10006 hashnncl 10039 fz1f1o 10572 nn0enne 10682 nn0o1gt2 10685 dfgcd2 10783 mulgcd 10785 eucalgf 10817 eucalginv 10818 prmdvdsexpr 10909 rpexp1i 10913 nn0gcdsq 10958 |
Copyright terms: Public domain | W3C validator |