Axiom ax-resscn 8277

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

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

This axiom is used by:  recn  8318  reex  8319  recni  8344  rerecapb  9181  nnsscn  9318  nn0sscn  9579  qsscn  10047  reexpcl  11014  rpexpcl  11016  reexpclzap  11017  expge0  11033  expge1  11034  abscn2  12106  recn2  12108  imcn2  12109  climabs  12111  climre  12113  climim  12114  climcvg1nlem  12140  fsumrecl  12193  fsumrpcl  12196  fsumge0  12251  fsumre  12264  fsumim  12265  fprodrecl  12400  fprodrpcl  12403  fprodreclf  12406  fprodge0  12429  fprodge1  12431  reeff1  12492  remet  15774  tgioo2cntop  15783  tgioo2  15785  abscncf  15811  recncf  15812  imcncf  15813  cnrehmeocntop  15836  maxcncf  15841  mincncf  15842  ivthreinc  15871  hovercncf  15872  limcimolemlt  15890  recnprss  15913  dvidrelem  15918  dvidre  15923  dvcjbr  15934  dvfre  15936  reeff1olem  15997  cosz12  16007  ioocosf1o  16082  efnnfsumcl  16239  efchtqdvds  16265