![]() |
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 7494. (Contributed by NM, 1-Mar-1995.) |
Ref | Expression |
---|---|
ax-resscn |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cr 7446 |
. 2
![]() ![]() | |
2 | cc 7445 |
. 2
![]() ![]() | |
3 | 1, 2 | wss 3013 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This axiom is referenced by: recn 7572 reex 7573 recni 7597 nnsscn 8525 nn0sscn 8776 qsscn 9215 reexpcl 10087 rpexpcl 10089 reexpclzap 10090 expge0 10106 expge1 10107 abscn2 10858 recn2 10860 imcn2 10861 climabs 10863 climre 10865 climim 10866 climcvg1nlem 10892 fsumrecl 10944 fsumrpcl 10947 fsumge0 11002 fsumre 11015 fsumim 11016 reeff1 11140 remet 12314 abscncf 12338 recncf 12339 imcncf 12340 |
Copyright terms: Public domain | W3C validator |