Axiom ax-resscn 8123

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 8030	. 2 class ℝ
2		cc 8029	. 2 class ℂ
3	1, 2	wss 3200	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  8164  reex  8165  recni  8190  rerecapb  9022  nnsscn  9147  nn0sscn  9406  qsscn  9864  reexpcl  10817  rpexpcl  10819  reexpclzap  10820  expge0  10836  expge1  10837  abscn2  11875  recn2  11877  imcn2  11878  climabs  11880  climre  11882  climim  11883  climcvg1nlem  11909  fsumrecl  11961  fsumrpcl  11964  fsumge0  12019  fsumre  12032  fsumim  12033  fprodrecl  12168  fprodrpcl  12171  fprodreclf  12174  fprodge0  12197  fprodge1  12199  reeff1  12260  remet  15271  tgioo2cntop  15280  tgioo2  15282  abscncf  15308  recncf  15309  imcncf  15310  cnrehmeocntop  15333  maxcncf  15338  mincncf  15339  ivthreinc  15368  hovercncf  15369  limcimolemlt  15387  recnprss  15410  dvidrelem  15415  dvidre  15420  dvcjbr  15431  dvfre  15433  reeff1olem  15494  cosz12  15503  ioocosf1o  15577