Axiom ax-resscn 7999

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 7906	. 2 class ℝ
2		cc 7905	. 2 class ℂ
3	1, 2	wss 3165	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  8040  reex  8041  recni  8066  rerecapb  8898  nnsscn  9023  nn0sscn  9282  qsscn  9734  reexpcl  10682  rpexpcl  10684  reexpclzap  10685  expge0  10701  expge1  10702  abscn2  11545  recn2  11547  imcn2  11548  climabs  11550  climre  11552  climim  11553  climcvg1nlem  11579  fsumrecl  11631  fsumrpcl  11634  fsumge0  11689  fsumre  11702  fsumim  11703  fprodrecl  11838  fprodrpcl  11841  fprodreclf  11844  fprodge0  11867  fprodge1  11869  reeff1  11930  remet  14938  tgioo2cntop  14947  tgioo2  14949  abscncf  14975  recncf  14976  imcncf  14977  cnrehmeocntop  15000  maxcncf  15005  mincncf  15006  ivthreinc  15035  hovercncf  15036  limcimolemlt  15054  recnprss  15077  dvidrelem  15082  dvidre  15087  dvcjbr  15098  dvfre  15100  reeff1olem  15161  cosz12  15170  ioocosf1o  15244