Axiom ax-resscn 8264

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

This axiom is referenced by:  recn  8305  reex  8306  recni  8331  rerecapb  9166  nnsscn  9291  nn0sscn  9550  qsscn  10013  reexpcl  10974  rpexpcl  10976  reexpclzap  10977  expge0  10993  expge1  10994  abscn2  12062  recn2  12064  imcn2  12065  climabs  12067  climre  12069  climim  12070  climcvg1nlem  12096  fsumrecl  12149  fsumrpcl  12152  fsumge0  12207  fsumre  12220  fsumim  12221  fprodrecl  12356  fprodrpcl  12359  fprodreclf  12362  fprodge0  12385  fprodge1  12387  reeff1  12448  remet  15575  tgioo2cntop  15584  tgioo2  15586  abscncf  15612  recncf  15613  imcncf  15614  cnrehmeocntop  15637  maxcncf  15642  mincncf  15643  ivthreinc  15672  hovercncf  15673  limcimolemlt  15691  recnprss  15714  dvidrelem  15719  dvidre  15724  dvcjbr  15735  dvfre  15737  reeff1olem  15798  cosz12  15807  ioocosf1o  15881