Axiom ax-resscn 7878

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 7785	. 2 class ℝ
2		cc 7784	. 2 class ℂ
3	1, 2	wss 3127	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  7919  reex  7920  recni  7944  rerecapb  8773  nnsscn  8897  nn0sscn  9154  qsscn  9604  reexpcl  10507  rpexpcl  10509  reexpclzap  10510  expge0  10526  expge1  10527  abscn2  11291  recn2  11293  imcn2  11294  climabs  11296  climre  11298  climim  11299  climcvg1nlem  11325  fsumrecl  11377  fsumrpcl  11380  fsumge0  11435  fsumre  11448  fsumim  11449  fprodrecl  11584  fprodrpcl  11587  fprodreclf  11590  fprodge0  11613  fprodge1  11615  reeff1  11676  remet  13611  tgioo2cntop  13620  abscncf  13643  recncf  13644  imcncf  13645  cnrehmeocntop  13664  limcimolemlt  13704  recnprss  13727  dvcjbr  13743  dvfre  13745  reeff1olem  13763  cosz12  13772  ioocosf1o  13846