Axiom ax-resscn 7988

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

This axiom is referenced by:  recn  8029  reex  8030  recni  8055  rerecapb  8887  nnsscn  9012  nn0sscn  9271  qsscn  9722  reexpcl  10665  rpexpcl  10667  reexpclzap  10668  expge0  10684  expge1  10685  abscn2  11497  recn2  11499  imcn2  11500  climabs  11502  climre  11504  climim  11505  climcvg1nlem  11531  fsumrecl  11583  fsumrpcl  11586  fsumge0  11641  fsumre  11654  fsumim  11655  fprodrecl  11790  fprodrpcl  11793  fprodreclf  11796  fprodge0  11819  fprodge1  11821  reeff1  11882  remet  14868  tgioo2cntop  14877  tgioo2  14879  abscncf  14905  recncf  14906  imcncf  14907  cnrehmeocntop  14930  maxcncf  14935  mincncf  14936  ivthreinc  14965  hovercncf  14966  limcimolemlt  14984  recnprss  15007  dvidrelem  15012  dvidre  15017  dvcjbr  15028  dvfre  15030  reeff1olem  15091  cosz12  15100  ioocosf1o  15174