Axiom ax-resscn 8052

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

This axiom is referenced by:  recn  8093  reex  8094  recni  8119  rerecapb  8951  nnsscn  9076  nn0sscn  9335  qsscn  9787  reexpcl  10738  rpexpcl  10740  reexpclzap  10741  expge0  10757  expge1  10758  abscn2  11741  recn2  11743  imcn2  11744  climabs  11746  climre  11748  climim  11749  climcvg1nlem  11775  fsumrecl  11827  fsumrpcl  11830  fsumge0  11885  fsumre  11898  fsumim  11899  fprodrecl  12034  fprodrpcl  12037  fprodreclf  12040  fprodge0  12063  fprodge1  12065  reeff1  12126  remet  15135  tgioo2cntop  15144  tgioo2  15146  abscncf  15172  recncf  15173  imcncf  15174  cnrehmeocntop  15197  maxcncf  15202  mincncf  15203  ivthreinc  15232  hovercncf  15233  limcimolemlt  15251  recnprss  15274  dvidrelem  15279  dvidre  15284  dvcjbr  15295  dvfre  15297  reeff1olem  15358  cosz12  15367  ioocosf1o  15441