Axiom ax-resscn 7712

Description: The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by theorem axresscn 7668. (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 7619	. 2 class RR
2		cc 7618	. 2 class CC
3	1, 2	wss 3071	1 wff RR C_ CC

This axiom is referenced by:  recn  7753  reex  7754  recni  7778  nnsscn  8725  nn0sscn  8982  qsscn  9423  reexpcl  10310  rpexpcl  10312  reexpclzap  10313  expge0  10329  expge1  10330  abscn2  11084  recn2  11086  imcn2  11087  climabs  11089  climre  11091  climim  11092  climcvg1nlem  11118  fsumrecl  11170  fsumrpcl  11173  fsumge0  11228  fsumre  11241  fsumim  11242  reeff1  11407  remet  12709  tgioo2cntop  12718  abscncf  12741  recncf  12742  imcncf  12743  cnrehmeocntop  12762  limcimolemlt  12802  recnprss  12825  dvcjbr  12841  dvfre  12843  cosz12  12861