![]() |
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 6936. (Contributed by NM, 1-Mar-1995.) |
Ref | Expression |
---|---|
ax-resscn |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cr 6888 |
. 2
![]() ![]() | |
2 | cc 6887 |
. 2
![]() ![]() | |
3 | 1, 2 | wss 2917 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This axiom is referenced by: recn 7014 reex 7015 recni 7039 nnsscn 7919 nn0sscn 8186 qsscn 8566 serige0 9252 serile 9253 reexpcl 9272 rpexpcl 9274 reexpclzap 9275 expge0 9291 expge1 9292 abscn2 9835 recn2 9837 imcn2 9838 climabs 9840 climre 9842 climim 9843 iserile 9862 climserile 9865 climcvg1nlem 9868 |
Copyright terms: Public domain | W3C validator |