Axiom ax-resscn 8221

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

This axiom is referenced by:  recn  8262  reex  8263  recni  8288  rerecapb  9119  nnsscn  9244  nn0sscn  9503  qsscn  9966  reexpcl  10922  rpexpcl  10924  reexpclzap  10925  expge0  10941  expge1  10942  abscn2  12004  recn2  12006  imcn2  12007  climabs  12009  climre  12011  climim  12012  climcvg1nlem  12038  fsumrecl  12091  fsumrpcl  12094  fsumge0  12149  fsumre  12162  fsumim  12163  fprodrecl  12298  fprodrpcl  12301  fprodreclf  12304  fprodge0  12327  fprodge1  12329  reeff1  12390  remet  15430  tgioo2cntop  15439  tgioo2  15441  abscncf  15467  recncf  15468  imcncf  15469  cnrehmeocntop  15492  maxcncf  15497  mincncf  15498  ivthreinc  15527  hovercncf  15528  limcimolemlt  15546  recnprss  15569  dvidrelem  15574  dvidre  15579  dvcjbr  15590  dvfre  15592  reeff1olem  15653  cosz12  15662  ioocosf1o  15736