Axiom ax-resscn 7966

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

This axiom is referenced by:  recn  8007  reex  8008  recni  8033  rerecapb  8864  nnsscn  8989  nn0sscn  9248  qsscn  9699  reexpcl  10630  rpexpcl  10632  reexpclzap  10633  expge0  10649  expge1  10650  abscn2  11461  recn2  11463  imcn2  11464  climabs  11466  climre  11468  climim  11469  climcvg1nlem  11495  fsumrecl  11547  fsumrpcl  11550  fsumge0  11605  fsumre  11618  fsumim  11619  fprodrecl  11754  fprodrpcl  11757  fprodreclf  11760  fprodge0  11783  fprodge1  11785  reeff1  11846  remet  14727  tgioo2cntop  14736  tgioo2  14738  abscncf  14764  recncf  14765  imcncf  14766  cnrehmeocntop  14789  maxcncf  14794  mincncf  14795  ivthreinc  14824  hovercncf  14825  limcimolemlt  14843  recnprss  14866  dvidrelem  14871  dvidre  14876  dvcjbr  14887  dvfre  14889  reeff1olem  14947  cosz12  14956  ioocosf1o  15030