![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > zex | GIF version |
Description: The set of integers exists. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Ref | Expression |
---|---|
zex | ⊢ ℤ ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnex 7563 | . 2 ⊢ ℂ ∈ V | |
2 | zsscn 8856 | . 2 ⊢ ℤ ⊆ ℂ | |
3 | 1, 2 | ssexi 3998 | 1 ⊢ ℤ ∈ V |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 1445 Vcvv 2633 ℂcc 7445 ℤcz 8848 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 ax-sep 3978 ax-cnex 7533 ax-resscn 7534 |
This theorem depends on definitions: df-bi 116 df-3or 928 df-3an 929 df-tru 1299 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-rex 2376 df-rab 2379 df-v 2635 df-un 3017 df-in 3019 df-ss 3026 df-sn 3472 df-pr 3473 df-op 3475 df-uni 3676 df-br 3868 df-iota 5014 df-fv 5057 df-ov 5693 df-neg 7753 df-z 8849 |
This theorem is referenced by: dfuzi 8955 uzval 9120 uzf 9121 fzval 9575 fzf 9577 flval 9828 frec2uzrand 9961 frec2uzf1od 9962 frecfzennn 9982 hashinfom 10317 climz 10851 serclim0 10864 climaddc1 10888 climmulc2 10890 climsubc1 10891 climsubc2 10892 climle 10893 climlec2 10900 iserabs 11034 isumshft 11049 explecnv 11064 qnumval 11606 qdenval 11607 znnen 11654 lmres 12115 climcncf 12353 |
Copyright terms: Public domain | W3C validator |