Axiom ax-resscn 8019

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

This axiom is referenced by:  recn  8060  reex  8061  recni  8086  rerecapb  8918  nnsscn  9043  nn0sscn  9302  qsscn  9754  reexpcl  10703  rpexpcl  10705  reexpclzap  10706  expge0  10722  expge1  10723  abscn2  11659  recn2  11661  imcn2  11662  climabs  11664  climre  11666  climim  11667  climcvg1nlem  11693  fsumrecl  11745  fsumrpcl  11748  fsumge0  11803  fsumre  11816  fsumim  11817  fprodrecl  11952  fprodrpcl  11955  fprodreclf  11958  fprodge0  11981  fprodge1  11983  reeff1  12044  remet  15053  tgioo2cntop  15062  tgioo2  15064  abscncf  15090  recncf  15091  imcncf  15092  cnrehmeocntop  15115  maxcncf  15120  mincncf  15121  ivthreinc  15150  hovercncf  15151  limcimolemlt  15169  recnprss  15192  dvidrelem  15197  dvidre  15202  dvcjbr  15213  dvfre  15215  reeff1olem  15276  cosz12  15285  ioocosf1o  15359