Axiom ax-resscn 7990

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 7897	. 2 class ℝ
2		cc 7896	. 2 class ℂ
3	1, 2	wss 3157	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  8031  reex  8032  recni  8057  rerecapb  8889  nnsscn  9014  nn0sscn  9273  qsscn  9724  reexpcl  10667  rpexpcl  10669  reexpclzap  10670  expge0  10686  expge1  10687  abscn2  11499  recn2  11501  imcn2  11502  climabs  11504  climre  11506  climim  11507  climcvg1nlem  11533  fsumrecl  11585  fsumrpcl  11588  fsumge0  11643  fsumre  11656  fsumim  11657  fprodrecl  11792  fprodrpcl  11795  fprodreclf  11798  fprodge0  11821  fprodge1  11823  reeff1  11884  remet  14892  tgioo2cntop  14901  tgioo2  14903  abscncf  14929  recncf  14930  imcncf  14931  cnrehmeocntop  14954  maxcncf  14959  mincncf  14960  ivthreinc  14989  hovercncf  14990  limcimolemlt  15008  recnprss  15031  dvidrelem  15036  dvidre  15041  dvcjbr  15052  dvfre  15054  reeff1olem  15115  cosz12  15124  ioocosf1o  15198