Axiom ax-resscn 8102

Description: The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by Theorem axresscn 8058. (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 8009	. 2 class RR
2		cc 8008	. 2 class CC
3	1, 2	wss 3197	1 wff RR C_ CC

This axiom is referenced by:  recn  8143  reex  8144  recni  8169  rerecapb  9001  nnsscn  9126  nn0sscn  9385  qsscn  9838  reexpcl  10790  rpexpcl  10792  reexpclzap  10793  expge0  10809  expge1  10810  abscn2  11842  recn2  11844  imcn2  11845  climabs  11847  climre  11849  climim  11850  climcvg1nlem  11876  fsumrecl  11928  fsumrpcl  11931  fsumge0  11986  fsumre  11999  fsumim  12000  fprodrecl  12135  fprodrpcl  12138  fprodreclf  12141  fprodge0  12164  fprodge1  12166  reeff1  12227  remet  15238  tgioo2cntop  15247  tgioo2  15249  abscncf  15275  recncf  15276  imcncf  15277  cnrehmeocntop  15300  maxcncf  15305  mincncf  15306  ivthreinc  15335  hovercncf  15336  limcimolemlt  15354  recnprss  15377  dvidrelem  15382  dvidre  15387  dvcjbr  15398  dvfre  15400  reeff1olem  15461  cosz12  15470  ioocosf1o  15544