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 7822. (Contributed by NM, 1-Mar-1995.) |
Ref | Expression |
---|---|
ax-resscn | ⊢ ℝ ⊆ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cr 7773 | . 2 class ℝ | |
2 | cc 7772 | . 2 class ℂ | |
3 | 1, 2 | wss 3121 | 1 wff ℝ ⊆ ℂ |
Colors of variables: wff set class |
This axiom is referenced by: recn 7907 reex 7908 recni 7932 nnsscn 8883 nn0sscn 9140 qsscn 9590 reexpcl 10493 rpexpcl 10495 reexpclzap 10496 expge0 10512 expge1 10513 abscn2 11278 recn2 11280 imcn2 11281 climabs 11283 climre 11285 climim 11286 climcvg1nlem 11312 fsumrecl 11364 fsumrpcl 11367 fsumge0 11422 fsumre 11435 fsumim 11436 fprodrecl 11571 fprodrpcl 11574 fprodreclf 11577 fprodge0 11600 fprodge1 11602 reeff1 11663 remet 13334 tgioo2cntop 13343 abscncf 13366 recncf 13367 imcncf 13368 cnrehmeocntop 13387 limcimolemlt 13427 recnprss 13450 dvcjbr 13466 dvfre 13468 reeff1olem 13486 cosz12 13495 ioocosf1o 13569 |
Copyright terms: Public domain | W3C validator |