Axiom ax-resscn 8091

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

This axiom is referenced by:  recn  8132  reex  8133  recni  8158  rerecapb  8990  nnsscn  9115  nn0sscn  9374  qsscn  9826  reexpcl  10778  rpexpcl  10780  reexpclzap  10781  expge0  10797  expge1  10798  abscn2  11826  recn2  11828  imcn2  11829  climabs  11831  climre  11833  climim  11834  climcvg1nlem  11860  fsumrecl  11912  fsumrpcl  11915  fsumge0  11970  fsumre  11983  fsumim  11984  fprodrecl  12119  fprodrpcl  12122  fprodreclf  12125  fprodge0  12148  fprodge1  12150  reeff1  12211  remet  15222  tgioo2cntop  15231  tgioo2  15233  abscncf  15259  recncf  15260  imcncf  15261  cnrehmeocntop  15284  maxcncf  15289  mincncf  15290  ivthreinc  15319  hovercncf  15320  limcimolemlt  15338  recnprss  15361  dvidrelem  15366  dvidre  15371  dvcjbr  15382  dvfre  15384  reeff1olem  15445  cosz12  15454  ioocosf1o  15528