Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ax-resscn | GIF version |
Description: The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by theorem axresscn 7636. (Contributed by NM, 1-Mar-1995.) |
Ref | Expression |
---|---|
ax-resscn | ⊢ ℝ ⊆ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cr 7587 | . 2 class ℝ | |
2 | cc 7586 | . 2 class ℂ | |
3 | 1, 2 | wss 3041 | 1 wff ℝ ⊆ ℂ |
Colors of variables: wff set class |
This axiom is referenced by: recn 7721 reex 7722 recni 7746 nnsscn 8689 nn0sscn 8940 qsscn 9379 reexpcl 10265 rpexpcl 10267 reexpclzap 10268 expge0 10284 expge1 10285 abscn2 11039 recn2 11041 imcn2 11042 climabs 11044 climre 11046 climim 11047 climcvg1nlem 11073 fsumrecl 11125 fsumrpcl 11128 fsumge0 11183 fsumre 11196 fsumim 11197 reeff1 11321 remet 12620 tgioo2cntop 12629 abscncf 12652 recncf 12653 imcncf 12654 cnrehmeocntop 12673 limcimolemlt 12713 recnprss 12736 dvcjbr 12752 dvfre 12754 cosz12 12772 |
Copyright terms: Public domain | W3C validator |