Axiom ax-resscn 8219

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

This axiom is referenced by:  recn  8260  reex  8261  recni  8286  rerecapb  9117  nnsscn  9242  nn0sscn  9501  qsscn  9963  reexpcl  10918  rpexpcl  10920  reexpclzap  10921  expge0  10937  expge1  10938  abscn2  11998  recn2  12000  imcn2  12001  climabs  12003  climre  12005  climim  12006  climcvg1nlem  12032  fsumrecl  12085  fsumrpcl  12088  fsumge0  12143  fsumre  12156  fsumim  12157  fprodrecl  12292  fprodrpcl  12295  fprodreclf  12298  fprodge0  12321  fprodge1  12323  reeff1  12384  remet  15411  tgioo2cntop  15420  tgioo2  15422  abscncf  15448  recncf  15449  imcncf  15450  cnrehmeocntop  15473  maxcncf  15478  mincncf  15479  ivthreinc  15508  hovercncf  15509  limcimolemlt  15527  recnprss  15550  dvidrelem  15555  dvidre  15560  dvcjbr  15571  dvfre  15573  reeff1olem  15634  cosz12  15643  ioocosf1o  15717