Axiom ax-resscn 8272

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 8179	. 2 class ℝ
2		cc 8178	. 2 class ℂ
3	1, 2	wss 3220	1 wff ℝ ⊆ ℂ

This axiom is used by:  recn  8313  reex  8314  recni  8339  rerecapb  9176  nnsscn  9312  nn0sscn  9573  qsscn  10041  reexpcl  11008  rpexpcl  11010  reexpclzap  11011  expge0  11027  expge1  11028  abscn2  12100  recn2  12102  imcn2  12103  climabs  12105  climre  12107  climim  12108  climcvg1nlem  12134  fsumrecl  12187  fsumrpcl  12190  fsumge0  12245  fsumre  12258  fsumim  12259  fprodrecl  12394  fprodrpcl  12397  fprodreclf  12400  fprodge0  12423  fprodge1  12425  reeff1  12486  remet  15748  tgioo2cntop  15757  tgioo2  15759  abscncf  15785  recncf  15786  imcncf  15787  cnrehmeocntop  15810  maxcncf  15815  mincncf  15816  ivthreinc  15845  hovercncf  15846  limcimolemlt  15864  recnprss  15887  dvidrelem  15892  dvidre  15897  dvcjbr  15908  dvfre  15910  reeff1olem  15971  cosz12  15981  ioocosf1o  16056  efnnfsumcl  16213  efchtqdvds  16239