Axiom ax-resscn 8277

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

This axiom is used by:  recn  8318  reex  8319  recni  8344  rerecapb  9181  nnsscn  9318  nn0sscn  9579  qsscn  10046  reexpcl  11013  rpexpcl  11015  reexpclzap  11016  expge0  11032  expge1  11033  abscn2  12105  recn2  12107  imcn2  12108  climabs  12110  climre  12112  climim  12113  climcvg1nlem  12139  fsumrecl  12192  fsumrpcl  12195  fsumge0  12250  fsumre  12263  fsumim  12264  fprodrecl  12399  fprodrpcl  12402  fprodreclf  12405  fprodge0  12428  fprodge1  12430  reeff1  12491  remet  15791  tgioo2cntop  15800  tgioo2  15802  abscncf  15828  recncf  15829  imcncf  15830  cnrehmeocntop  15853  maxcncf  15858  mincncf  15859  ivthreinc  15888  hovercncf  15889  limcimolemlt  15907  recnprss  15930  dvidrelem  15935  dvidre  15940  dvcjbr  15951  dvfre  15953  reeff1olem  16014  cosz12  16024  ioocosf1o  16099  efnnfsumcl  16256  efchtqdvds  16282