Axiom ax-resscn 7903

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 7810	. 2 class ℝ
2		cc 7809	. 2 class ℂ
3	1, 2	wss 3130	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  7944  reex  7945  recni  7969  rerecapb  8800  nnsscn  8924  nn0sscn  9181  qsscn  9631  reexpcl  10537  rpexpcl  10539  reexpclzap  10540  expge0  10556  expge1  10557  abscn2  11323  recn2  11325  imcn2  11326  climabs  11328  climre  11330  climim  11331  climcvg1nlem  11357  fsumrecl  11409  fsumrpcl  11412  fsumge0  11467  fsumre  11480  fsumim  11481  fprodrecl  11616  fprodrpcl  11619  fprodreclf  11622  fprodge0  11645  fprodge1  11647  reeff1  11708  remet  14043  tgioo2cntop  14052  abscncf  14075  recncf  14076  imcncf  14077  cnrehmeocntop  14096  limcimolemlt  14136  recnprss  14159  dvcjbr  14175  dvfre  14177  reeff1olem  14195  cosz12  14204  ioocosf1o  14278