Axiom ax-resscn 7932

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

This axiom is referenced by:  recn  7973  reex  7974  recni  7998  rerecapb  8829  nnsscn  8953  nn0sscn  9210  qsscn  9660  reexpcl  10567  rpexpcl  10569  reexpclzap  10570  expge0  10586  expge1  10587  abscn2  11354  recn2  11356  imcn2  11357  climabs  11359  climre  11361  climim  11362  climcvg1nlem  11388  fsumrecl  11440  fsumrpcl  11443  fsumge0  11498  fsumre  11511  fsumim  11512  fprodrecl  11647  fprodrpcl  11650  fprodreclf  11653  fprodge0  11676  fprodge1  11678  reeff1  11739  remet  14492  tgioo2cntop  14501  abscncf  14524  recncf  14525  imcncf  14526  cnrehmeocntop  14545  limcimolemlt  14585  recnprss  14608  dvcjbr  14624  dvfre  14626  reeff1olem  14644  cosz12  14653  ioocosf1o  14727