Axiom ax-resscn 8037

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 7944	. 2 class ℝ
2		cc 7943	. 2 class ℂ
3	1, 2	wss 3170	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  8078  reex  8079  recni  8104  rerecapb  8936  nnsscn  9061  nn0sscn  9320  qsscn  9772  reexpcl  10723  rpexpcl  10725  reexpclzap  10726  expge0  10742  expge1  10743  abscn2  11701  recn2  11703  imcn2  11704  climabs  11706  climre  11708  climim  11709  climcvg1nlem  11735  fsumrecl  11787  fsumrpcl  11790  fsumge0  11845  fsumre  11858  fsumim  11859  fprodrecl  11994  fprodrpcl  11997  fprodreclf  12000  fprodge0  12023  fprodge1  12025  reeff1  12086  remet  15095  tgioo2cntop  15104  tgioo2  15106  abscncf  15132  recncf  15133  imcncf  15134  cnrehmeocntop  15157  maxcncf  15162  mincncf  15163  ivthreinc  15192  hovercncf  15193  limcimolemlt  15211  recnprss  15234  dvidrelem  15239  dvidre  15244  dvcjbr  15255  dvfre  15257  reeff1olem  15318  cosz12  15327  ioocosf1o  15401