Axiom ax-resscn 8102

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

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

This axiom is referenced by:  recn  8143  reex  8144  recni  8169  rerecapb  9001  nnsscn  9126  nn0sscn  9385  qsscn  9838  reexpcl  10790  rpexpcl  10792  reexpclzap  10793  expge0  10809  expge1  10810  abscn2  11841  recn2  11843  imcn2  11844  climabs  11846  climre  11848  climim  11849  climcvg1nlem  11875  fsumrecl  11927  fsumrpcl  11930  fsumge0  11985  fsumre  11998  fsumim  11999  fprodrecl  12134  fprodrpcl  12137  fprodreclf  12140  fprodge0  12163  fprodge1  12165  reeff1  12226  remet  15237  tgioo2cntop  15246  tgioo2  15248  abscncf  15274  recncf  15275  imcncf  15276  cnrehmeocntop  15299  maxcncf  15304  mincncf  15305  ivthreinc  15334  hovercncf  15335  limcimolemlt  15353  recnprss  15376  dvidrelem  15381  dvidre  15386  dvcjbr  15397  dvfre  15399  reeff1olem  15460  cosz12  15469  ioocosf1o  15543