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  15740  tgioo2cntop  15749  tgioo2  15751  abscncf  15777  recncf  15778  imcncf  15779  cnrehmeocntop  15802  maxcncf  15807  mincncf  15808  ivthreinc  15837  hovercncf  15838  limcimolemlt  15856  recnprss  15879  dvidrelem  15884  dvidre  15889  dvcjbr  15900  dvfre  15902  reeff1olem  15963  cosz12  15973  ioocosf1o  16047  efnnfsumcl  16200  efchtqdvds  16226