![]() |
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 9153 | . . 3 ⊢ ℕ0 = (ℕ ∪ {0}) | |
2 | 1 | eleq2i 2244 | . 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0})) |
3 | elun 3276 | . 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0})) | |
4 | c0ex 7929 | . . . 4 ⊢ 0 ∈ V | |
5 | 4 | elsn2 3625 | . . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0) |
6 | 5 | orbi2i 762 | . 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0)) |
7 | 2, 3, 6 | 3bitri 206 | 1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0)) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 ∨ wo 708 = wceq 1353 ∈ wcel 2148 ∪ cun 3127 {csn 3591 0cc0 7789 ℕcn 8895 ℕ0cn0 9152 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 ax-1cn 7882 ax-icn 7884 ax-addcl 7885 ax-mulcl 7887 ax-i2m1 7894 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-v 2739 df-un 3133 df-sn 3597 df-n0 9153 |
This theorem is referenced by: 0nn0 9167 nn0ge0 9177 nnnn0addcl 9182 nnm1nn0 9193 elnnnn0b 9196 elnn0z 9242 elznn0nn 9243 elznn0 9244 elznn 9245 nn0ind-raph 9346 nn0ledivnn 9741 expp1 10500 expnegap0 10501 expcllem 10504 nn0ltexp2 10661 facp1 10681 faclbnd 10692 faclbnd3 10694 bcn1 10709 bcval5 10714 hashnncl 10746 fz1f1o 11354 arisum 11477 arisum2 11478 fprodfac 11594 ef0lem 11639 nn0enne 11877 nn0o1gt2 11880 dfgcd2 11985 mulgcd 11987 eucalgf 12025 eucalginv 12026 prmdvdsexpr 12120 rpexp1i 12124 nn0gcdsq 12170 odzdvds 12215 pceq0 12291 fldivp1 12316 pockthg 12325 1arith 12335 mulgnn0p1 12870 mulgnn0subcl 12872 mulgneg 12877 mulgnn0z 12885 mulgnn0dir 12888 mulgnn0ass 12894 dvexp2 13809 lgsdir 14069 lgsabs1 14073 2sqlem7 14090 |
Copyright terms: Public domain | W3C validator |