Axiom ax-resscn 7841

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

This axiom is referenced by:  recn  7882  reex  7883  recni  7907  nnsscn  8858  nn0sscn  9115  qsscn  9565  reexpcl  10468  rpexpcl  10470  reexpclzap  10471  expge0  10487  expge1  10488  abscn2  11252  recn2  11254  imcn2  11255  climabs  11257  climre  11259  climim  11260  climcvg1nlem  11286  fsumrecl  11338  fsumrpcl  11341  fsumge0  11396  fsumre  11409  fsumim  11410  fprodrecl  11545  fprodrpcl  11548  fprodreclf  11551  fprodge0  11574  fprodge1  11576  reeff1  11637  remet  13140  tgioo2cntop  13149  abscncf  13172  recncf  13173  imcncf  13174  cnrehmeocntop  13193  limcimolemlt  13233  recnprss  13256  dvcjbr  13272  dvfre  13274  reeff1olem  13292  cosz12  13301  ioocosf1o  13375