Axiom ax-resscn 8087

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 7994	. 2 class ℝ
2		cc 7993	. 2 class ℂ
3	1, 2	wss 3197	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  8128  reex  8129  recni  8154  rerecapb  8986  nnsscn  9111  nn0sscn  9370  qsscn  9822  reexpcl  10773  rpexpcl  10775  reexpclzap  10776  expge0  10792  expge1  10793  abscn2  11821  recn2  11823  imcn2  11824  climabs  11826  climre  11828  climim  11829  climcvg1nlem  11855  fsumrecl  11907  fsumrpcl  11910  fsumge0  11965  fsumre  11978  fsumim  11979  fprodrecl  12114  fprodrpcl  12117  fprodreclf  12120  fprodge0  12143  fprodge1  12145  reeff1  12206  remet  15216  tgioo2cntop  15225  tgioo2  15227  abscncf  15253  recncf  15254  imcncf  15255  cnrehmeocntop  15278  maxcncf  15283  mincncf  15284  ivthreinc  15313  hovercncf  15314  limcimolemlt  15332  recnprss  15355  dvidrelem  15360  dvidre  15365  dvcjbr  15376  dvfre  15378  reeff1olem  15439  cosz12  15448  ioocosf1o  15522