Axiom ax-resscn 7971

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

This axiom is referenced by:  recn  8012  reex  8013  recni  8038  rerecapb  8870  nnsscn  8995  nn0sscn  9254  qsscn  9705  reexpcl  10648  rpexpcl  10650  reexpclzap  10651  expge0  10667  expge1  10668  abscn2  11480  recn2  11482  imcn2  11483  climabs  11485  climre  11487  climim  11488  climcvg1nlem  11514  fsumrecl  11566  fsumrpcl  11569  fsumge0  11624  fsumre  11637  fsumim  11638  fprodrecl  11773  fprodrpcl  11776  fprodreclf  11779  fprodge0  11802  fprodge1  11804  reeff1  11865  remet  14784  tgioo2cntop  14793  tgioo2  14795  abscncf  14821  recncf  14822  imcncf  14823  cnrehmeocntop  14846  maxcncf  14851  mincncf  14852  ivthreinc  14881  hovercncf  14882  limcimolemlt  14900  recnprss  14923  dvidrelem  14928  dvidre  14933  dvcjbr  14944  dvfre  14946  reeff1olem  15007  cosz12  15016  ioocosf1o  15090