![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nnex | GIF version |
Description: The set of positive integers exists. (Contributed by NM, 3-Oct-1999.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Ref | Expression |
---|---|
nnex | ⊢ ℕ ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnex 7934 | . 2 ⊢ ℂ ∈ V | |
2 | nnsscn 8923 | . 2 ⊢ ℕ ⊆ ℂ | |
3 | 1, 2 | ssexi 4141 | 1 ⊢ ℕ ∈ V |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 2148 Vcvv 2737 ℂcc 7808 ℕcn 8918 |
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-sep 4121 ax-cnex 7901 ax-resscn 7902 ax-1re 7904 ax-addrcl 7907 |
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-ral 2460 df-v 2739 df-in 3135 df-ss 3142 df-int 3845 df-inn 8919 |
This theorem is referenced by: nn0ex 9181 nn0ennn 10432 climrecvg1n 11355 climcvg1nlem 11356 divcnv 11504 trireciplem 11507 expcnvap0 11509 expcnv 11511 geo2lim 11523 prmex 12112 qnumval 12184 qdenval 12185 oddennn 12392 evenennn 12393 xpnnen 12394 znnen 12398 qnnen 12431 ssnnctlemct 12446 nninfdc 12453 ndxarg 12484 trilpo 14727 redcwlpo 14739 nconstwlpo 14749 neapmkv 14751 |
Copyright terms: Public domain | W3C validator |