Axiom ax-resscn 8271

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 8178	. 2 class ℝ
2		cc 8177	. 2 class ℂ
3	1, 2	wss 3220	1 wff ℝ ⊆ ℂ

This axiom is used by:  recn  8312  reex  8313  recni  8338  rerecapb  9173  nnsscn  9309  nn0sscn  9568  qsscn  10031  reexpcl  10993  rpexpcl  10995  reexpclzap  10996  expge0  11012  expge1  11013  abscn2  12081  recn2  12083  imcn2  12084  climabs  12086  climre  12088  climim  12089  climcvg1nlem  12115  fsumrecl  12168  fsumrpcl  12171  fsumge0  12226  fsumre  12239  fsumim  12240  fprodrecl  12375  fprodrpcl  12378  fprodreclf  12381  fprodge0  12404  fprodge1  12406  reeff1  12467  remet  15649  tgioo2cntop  15658  tgioo2  15660  abscncf  15686  recncf  15687  imcncf  15688  cnrehmeocntop  15711  maxcncf  15716  mincncf  15717  ivthreinc  15746  hovercncf  15747  limcimolemlt  15765  recnprss  15788  dvidrelem  15793  dvidre  15798  dvcjbr  15809  dvfre  15811  reeff1olem  15872  cosz12  15881  ioocosf1o  15955