Axiom ax-resscn 7845

Description: The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by Theorem axresscn 7801. (Contributed by NM, 1-Mar-1995.)

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 7752	. 2 class ℝ
2		cc 7751	. 2 class ℂ
3	1, 2	wss 3116	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  7886  reex  7887  recni  7911  nnsscn  8862  nn0sscn  9119  qsscn  9569  reexpcl  10472  rpexpcl  10474  reexpclzap  10475  expge0  10491  expge1  10492  abscn2  11256  recn2  11258  imcn2  11259  climabs  11261  climre  11263  climim  11264  climcvg1nlem  11290  fsumrecl  11342  fsumrpcl  11345  fsumge0  11400  fsumre  11413  fsumim  11414  fprodrecl  11549  fprodrpcl  11552  fprodreclf  11555  fprodge0  11578  fprodge1  11580  reeff1  11641  remet  13180  tgioo2cntop  13189  abscncf  13212  recncf  13213  imcncf  13214  cnrehmeocntop  13233  limcimolemlt  13273  recnprss  13296  dvcjbr  13312  dvfre  13314  reeff1olem  13332  cosz12  13341  ioocosf1o  13415