Axiom ax-resscn 8114

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 8021	. 2 class ℝ
2		cc 8020	. 2 class ℂ
3	1, 2	wss 3198	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  8155  reex  8156  recni  8181  rerecapb  9013  nnsscn  9138  nn0sscn  9397  qsscn  9855  reexpcl  10808  rpexpcl  10810  reexpclzap  10811  expge0  10827  expge1  10828  abscn2  11866  recn2  11868  imcn2  11869  climabs  11871  climre  11873  climim  11874  climcvg1nlem  11900  fsumrecl  11952  fsumrpcl  11955  fsumge0  12010  fsumre  12023  fsumim  12024  fprodrecl  12159  fprodrpcl  12162  fprodreclf  12165  fprodge0  12188  fprodge1  12190  reeff1  12251  remet  15262  tgioo2cntop  15271  tgioo2  15273  abscncf  15299  recncf  15300  imcncf  15301  cnrehmeocntop  15324  maxcncf  15329  mincncf  15330  ivthreinc  15359  hovercncf  15360  limcimolemlt  15378  recnprss  15401  dvidrelem  15406  dvidre  15411  dvcjbr  15422  dvfre  15424  reeff1olem  15485  cosz12  15494  ioocosf1o  15568