Axiom ax-resscn 7938

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 7845	. 2 class ℝ
2		cc 7844	. 2 class ℂ
3	1, 2	wss 3144	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  7979  reex  7980  recni  8004  rerecapb  8835  nnsscn  8959  nn0sscn  9216  qsscn  9667  reexpcl  10577  rpexpcl  10579  reexpclzap  10580  expge0  10596  expge1  10597  abscn2  11364  recn2  11366  imcn2  11367  climabs  11369  climre  11371  climim  11372  climcvg1nlem  11398  fsumrecl  11450  fsumrpcl  11453  fsumge0  11508  fsumre  11521  fsumim  11522  fprodrecl  11657  fprodrpcl  11660  fprodreclf  11663  fprodge0  11686  fprodge1  11688  reeff1  11749  remet  14525  tgioo2cntop  14534  abscncf  14557  recncf  14558  imcncf  14559  cnrehmeocntop  14578  limcimolemlt  14618  recnprss  14641  dvcjbr  14657  dvfre  14659  reeff1olem  14677  cosz12  14686  ioocosf1o  14760