Axiom ax-resscn 8235

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

This axiom is referenced by:  recn  8276  reex  8277  recni  8302  rerecapb  9134  nnsscn  9259  nn0sscn  9518  qsscn  9981  reexpcl  10942  rpexpcl  10944  reexpclzap  10945  expge0  10961  expge1  10962  abscn2  12025  recn2  12027  imcn2  12028  climabs  12030  climre  12032  climim  12033  climcvg1nlem  12059  fsumrecl  12112  fsumrpcl  12115  fsumge0  12170  fsumre  12183  fsumim  12184  fprodrecl  12319  fprodrpcl  12322  fprodreclf  12325  fprodge0  12348  fprodge1  12350  reeff1  12411  remet  15539  tgioo2cntop  15548  tgioo2  15550  abscncf  15576  recncf  15577  imcncf  15578  cnrehmeocntop  15601  maxcncf  15606  mincncf  15607  ivthreinc  15636  hovercncf  15637  limcimolemlt  15655  recnprss  15678  dvidrelem  15683  dvidre  15688  dvcjbr  15699  dvfre  15701  reeff1olem  15762  cosz12  15771  ioocosf1o  15845