Axiom ax-resscn 7068

Description: The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by theorem axresscn 7028. (Contributed by NM, 1-Mar-1995.)

Assertion

Ref	Expression
ax-resscn	|- RR C_ CC

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 6980	. 2 class RR
2		cc 6979	. 2 class CC
3	1, 2	wss 2973	1 wff RR C_ CC

This axiom is referenced by:  recn  7106  reex  7107  recni  7131  nnsscn  8044  nn0sscn  8293  qsscn  8716  serige0  9473  serile  9474  reexpcl  9493  rpexpcl  9495  reexpclzap  9496  expge0  9512  expge1  9513  abscn2  10153  recn2  10155  imcn2  10156  climabs  10158  climre  10160  climim  10161  iserile  10180  climserile  10183  climcvg1nlem  10186