![]() |
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 7589. (Contributed by NM, 1-Mar-1995.) |
Ref | Expression |
---|---|
ax-resscn | ⊢ ℝ ⊆ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cr 7540 | . 2 class ℝ | |
2 | cc 7539 | . 2 class ℂ | |
3 | 1, 2 | wss 3035 | 1 wff ℝ ⊆ ℂ |
Colors of variables: wff set class |
This axiom is referenced by: recn 7671 reex 7672 recni 7696 nnsscn 8629 nn0sscn 8880 qsscn 9319 reexpcl 10197 rpexpcl 10199 reexpclzap 10200 expge0 10216 expge1 10217 abscn2 10970 recn2 10972 imcn2 10973 climabs 10975 climre 10977 climim 10978 climcvg1nlem 11004 fsumrecl 11056 fsumrpcl 11059 fsumge0 11114 fsumre 11127 fsumim 11128 reeff1 11252 remet 12520 tgioo2cntop 12529 abscncf 12552 recncf 12553 imcncf 12554 limcimolemlt 12583 recnprss 12605 |
Copyright terms: Public domain | W3C validator |