![]() |
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 7160. (Contributed by NM, 1-Mar-1995.) |
Ref | Expression |
---|---|
ax-resscn |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cr 7112 |
. 2
![]() ![]() | |
2 | cc 7111 |
. 2
![]() ![]() | |
3 | 1, 2 | wss 2982 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This axiom is referenced by: recn 7238 reex 7239 recni 7263 nnsscn 8181 nn0sscn 8430 qsscn 8867 serige0 9640 serile 9641 reexpcl 9660 rpexpcl 9662 reexpclzap 9663 expge0 9679 expge1 9680 abscn2 10372 recn2 10374 imcn2 10375 climabs 10377 climre 10379 climim 10380 iserile 10399 climserile 10402 climcvg1nlem 10405 |
Copyright terms: Public domain | W3C validator |