Axiom ax-resscn 7905

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

This axiom is referenced by:  recn  7946  reex  7947  recni  7971  rerecapb  8802  nnsscn  8926  nn0sscn  9183  qsscn  9633  reexpcl  10539  rpexpcl  10541  reexpclzap  10542  expge0  10558  expge1  10559  abscn2  11325  recn2  11327  imcn2  11328  climabs  11330  climre  11332  climim  11333  climcvg1nlem  11359  fsumrecl  11411  fsumrpcl  11414  fsumge0  11469  fsumre  11482  fsumim  11483  fprodrecl  11618  fprodrpcl  11621  fprodreclf  11624  fprodge0  11647  fprodge1  11649  reeff1  11710  remet  14079  tgioo2cntop  14088  abscncf  14111  recncf  14112  imcncf  14113  cnrehmeocntop  14132  limcimolemlt  14172  recnprss  14195  dvcjbr  14211  dvfre  14213  reeff1olem  14231  cosz12  14240  ioocosf1o  14314