![]() |
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 7894. (Contributed by NM, 1-Mar-1995.) |
Ref | Expression |
---|---|
ax-resscn | ⊢ ℝ ⊆ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cr 7845 | . 2 class ℝ | |
2 | cc 7844 | . 2 class ℂ | |
3 | 1, 2 | wss 3144 | 1 wff ℝ ⊆ ℂ |
Colors of variables: wff set class |
This axiom is referenced by: recn 7979 reex 7980 recni 8004 rerecapb 8835 nnsscn 8959 nn0sscn 9216 qsscn 9667 reexpcl 10577 rpexpcl 10579 reexpclzap 10580 expge0 10596 expge1 10597 abscn2 11364 recn2 11366 imcn2 11367 climabs 11369 climre 11371 climim 11372 climcvg1nlem 11398 fsumrecl 11450 fsumrpcl 11453 fsumge0 11508 fsumre 11521 fsumim 11522 fprodrecl 11657 fprodrpcl 11660 fprodreclf 11663 fprodge0 11686 fprodge1 11688 reeff1 11749 remet 14525 tgioo2cntop 14534 abscncf 14557 recncf 14558 imcncf 14559 cnrehmeocntop 14578 limcimolemlt 14618 recnprss 14641 dvcjbr 14657 dvfre 14659 reeff1olem 14677 cosz12 14686 ioocosf1o 14760 |
Copyright terms: Public domain | W3C validator |