Axiom ax-resscn 8271

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

This axiom is used by:  recn  8312  reex  8313  recni  8338  rerecapb  9175  nnsscn  9311  nn0sscn  9572  qsscn  10040  reexpcl  11006  rpexpcl  11008  reexpclzap  11009  expge0  11025  expge1  11026  abscn2  12097  recn2  12099  imcn2  12100  climabs  12102  climre  12104  climim  12105  climcvg1nlem  12131  fsumrecl  12184  fsumrpcl  12187  fsumge0  12242  fsumre  12255  fsumim  12256  fprodrecl  12391  fprodrpcl  12394  fprodreclf  12397  fprodge0  12420  fprodge1  12422  reeff1  12483  remet  15698  tgioo2cntop  15707  tgioo2  15709  abscncf  15735  recncf  15736  imcncf  15737  cnrehmeocntop  15760  maxcncf  15765  mincncf  15766  ivthreinc  15795  hovercncf  15796  limcimolemlt  15814  recnprss  15837  dvidrelem  15842  dvidre  15847  dvcjbr  15858  dvfre  15860  reeff1olem  15921  cosz12  15931  ioocosf1o  16005