Axiom ax-resscn 7964

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

This axiom is referenced by:  recn  8005  reex  8006  recni  8031  rerecapb  8862  nnsscn  8987  nn0sscn  9245  qsscn  9696  reexpcl  10627  rpexpcl  10629  reexpclzap  10630  expge0  10646  expge1  10647  abscn2  11458  recn2  11460  imcn2  11461  climabs  11463  climre  11465  climim  11466  climcvg1nlem  11492  fsumrecl  11544  fsumrpcl  11547  fsumge0  11602  fsumre  11615  fsumim  11616  fprodrecl  11751  fprodrpcl  11754  fprodreclf  11757  fprodge0  11780  fprodge1  11782  reeff1  11843  remet  14708  tgioo2cntop  14717  abscncf  14740  recncf  14741  imcncf  14742  cnrehmeocntop  14764  maxcncf  14769  mincncf  14770  ivthreinc  14799  hovercncf  14800  limcimolemlt  14818  recnprss  14841  dvcjbr  14857  dvfre  14859  reeff1olem  14906  cosz12  14915  ioocosf1o  14989