Axiom ax-resscn 7631

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 7540	. 2 class ℝ
2		cc 7539	. 2 class ℂ
3	1, 2	wss 3035	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  7671  reex  7672  recni  7696  nnsscn  8629  nn0sscn  8880  qsscn  9319  reexpcl  10197  rpexpcl  10199  reexpclzap  10200  expge0  10216  expge1  10217  abscn2  10970  recn2  10972  imcn2  10973  climabs  10975  climre  10977  climim  10978  climcvg1nlem  11004  fsumrecl  11056  fsumrpcl  11059  fsumge0  11114  fsumre  11127  fsumim  11128  reeff1  11252  remet  12520  tgioo2cntop  12529  abscncf  12552  recncf  12553  imcncf  12554  limcimolemlt  12583  recnprss  12605