Axiom ax-resscn 7736

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

This axiom is referenced by:  recn  7777  reex  7778  recni  7802  nnsscn  8749  nn0sscn  9006  qsscn  9450  reexpcl  10341  rpexpcl  10343  reexpclzap  10344  expge0  10360  expge1  10361  abscn2  11116  recn2  11118  imcn2  11119  climabs  11121  climre  11123  climim  11124  climcvg1nlem  11150  fsumrecl  11202  fsumrpcl  11205  fsumge0  11260  fsumre  11273  fsumim  11274  reeff1  11443  remet  12748  tgioo2cntop  12757  abscncf  12780  recncf  12781  imcncf  12782  cnrehmeocntop  12801  limcimolemlt  12841  recnprss  12864  dvcjbr  12880  dvfre  12882  reeff1olem  12900  cosz12  12909  ioocosf1o  12983