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 7792. (Contributed by NM, 1-Mar-1995.) |
Ref | Expression |
---|---|
ax-resscn | ⊢ ℝ ⊆ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cr 7743 | . 2 class ℝ | |
2 | cc 7742 | . 2 class ℂ | |
3 | 1, 2 | wss 3111 | 1 wff ℝ ⊆ ℂ |
Colors of variables: wff set class |
This axiom is referenced by: recn 7877 reex 7878 recni 7902 nnsscn 8853 nn0sscn 9110 qsscn 9560 reexpcl 10462 rpexpcl 10464 reexpclzap 10465 expge0 10481 expge1 10482 abscn2 11242 recn2 11244 imcn2 11245 climabs 11247 climre 11249 climim 11250 climcvg1nlem 11276 fsumrecl 11328 fsumrpcl 11331 fsumge0 11386 fsumre 11399 fsumim 11400 fprodrecl 11535 fprodrpcl 11538 fprodreclf 11541 fprodge0 11564 fprodge1 11566 reeff1 11627 remet 13087 tgioo2cntop 13096 abscncf 13119 recncf 13120 imcncf 13121 cnrehmeocntop 13140 limcimolemlt 13180 recnprss 13203 dvcjbr 13219 dvfre 13221 reeff1olem 13239 cosz12 13248 ioocosf1o 13322 |
Copyright terms: Public domain | W3C validator |