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 9106 | . . 3 ⊢ ℕ0 = (ℕ ∪ {0}) | |
2 | 1 | eleq2i 2231 | . 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0})) |
3 | elun 3258 | . 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0})) | |
4 | c0ex 7884 | . . . 4 ⊢ 0 ∈ V | |
5 | 4 | elsn2 3604 | . . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0) |
6 | 5 | orbi2i 752 | . 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0)) |
7 | 2, 3, 6 | 3bitri 205 | 1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0)) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ∨ wo 698 = wceq 1342 ∈ wcel 2135 ∪ cun 3109 {csn 3570 0cc0 7744 ℕcn 8848 ℕ0cn0 9105 |
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 699 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 ax-1cn 7837 ax-icn 7839 ax-addcl 7840 ax-mulcl 7842 ax-i2m1 7849 |
This theorem depends on definitions: df-bi 116 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-v 2723 df-un 3115 df-sn 3576 df-n0 9106 |
This theorem is referenced by: 0nn0 9120 nn0ge0 9130 nnnn0addcl 9135 nnm1nn0 9146 elnnnn0b 9149 elnn0z 9195 elznn0nn 9196 elznn0 9197 elznn 9198 nn0ind-raph 9299 nn0ledivnn 9694 expp1 10452 expnegap0 10453 expcllem 10456 nn0ltexp2 10612 facp1 10632 faclbnd 10643 faclbnd3 10645 bcn1 10660 bcval5 10665 hashnncl 10698 fz1f1o 11302 arisum 11425 arisum2 11426 fprodfac 11542 ef0lem 11587 nn0enne 11824 nn0o1gt2 11827 dfgcd2 11932 mulgcd 11934 eucalgf 11966 eucalginv 11967 prmdvdsexpr 12061 rpexp1i 12065 nn0gcdsq 12111 odzdvds 12156 pceq0 12232 fldivp1 12257 pockthg 12266 dvexp2 13223 |
Copyright terms: Public domain | W3C validator |