Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ax-resscn | Unicode version |
Description: The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by theorem axresscn 7668. (Contributed by NM, 1-Mar-1995.) |
Ref | Expression |
---|---|
ax-resscn |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cr 7619 | . 2 | |
2 | cc 7618 | . 2 | |
3 | 1, 2 | wss 3071 | 1 |
Colors of variables: wff set class |
This axiom is referenced by: recn 7753 reex 7754 recni 7778 nnsscn 8725 nn0sscn 8982 qsscn 9423 reexpcl 10310 rpexpcl 10312 reexpclzap 10313 expge0 10329 expge1 10330 abscn2 11084 recn2 11086 imcn2 11087 climabs 11089 climre 11091 climim 11092 climcvg1nlem 11118 fsumrecl 11170 fsumrpcl 11173 fsumge0 11228 fsumre 11241 fsumim 11242 reeff1 11407 remet 12709 tgioo2cntop 12718 abscncf 12741 recncf 12742 imcncf 12743 cnrehmeocntop 12762 limcimolemlt 12802 recnprss 12825 dvcjbr 12841 dvfre 12843 cosz12 12861 |
Copyright terms: Public domain | W3C validator |