Axiom ax-resscn 8124

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

This axiom is referenced by:  recn  8165  reex  8166  recni  8191  rerecapb  9023  nnsscn  9148  nn0sscn  9407  qsscn  9865  reexpcl  10819  rpexpcl  10821  reexpclzap  10822  expge0  10838  expge1  10839  abscn2  11893  recn2  11895  imcn2  11896  climabs  11898  climre  11900  climim  11901  climcvg1nlem  11927  fsumrecl  11980  fsumrpcl  11983  fsumge0  12038  fsumre  12051  fsumim  12052  fprodrecl  12187  fprodrpcl  12190  fprodreclf  12193  fprodge0  12216  fprodge1  12218  reeff1  12279  remet  15291  tgioo2cntop  15300  tgioo2  15302  abscncf  15328  recncf  15329  imcncf  15330  cnrehmeocntop  15353  maxcncf  15358  mincncf  15359  ivthreinc  15388  hovercncf  15389  limcimolemlt  15407  recnprss  15430  dvidrelem  15435  dvidre  15440  dvcjbr  15451  dvfre  15453  reeff1olem  15514  cosz12  15523  ioocosf1o  15597