Axiom ax-resscn 11092

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 11034	. 2 class ℝ
2		cc 11033	. 2 class ℂ
3	1, 2	wss 3890	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  11125  reex  11126  recni  11156  qsscn  12907  ioosscn  13358  unitsscn  13450  reexpcl  14037  rpexpcl  14039  reexpclz  14041  expge0  14057  expge1  14058  rlimrecl  15539  abscn2  15558  recn2  15560  imcn2  15561  climabs  15563  climre  15565  climim  15566  rlimabs  15568  rlimre  15570  rlimim  15571  caurcvgr  15633  caucvgrlem2  15634  caurcvg  15636  fsumrecl  15693  fsumrpcl  15696  fsumge0  15755  fsumre  15768  fsumim  15769  fprodrecl  15915  fprodrpcl  15918  fprodreclf  15921  fprodge0  15955  fprodge1  15957  rerisefaccl  15979  refallfaccl  15980  rprisefaccl  15985  reeff1  16084  nthruc  16216  regsumfsum  21412  rge0srg  21415  rebase  21583  re0g  21589  regsumsupp  21599  remet  24752  tgioo2  24765  xrsdsre  24773  recld2  24777  reperf  24782  iitopon  24843  dfii3  24847  abscncf  24865  recncf  24866  imcncf  24867  abscncfALT  24888  cnmptre  24891  icchmeo  24905  cnrehmeo  24917  evth  24923  evth2  24924  lebnumlem2  24926  lebnumii  24930  cphsqrtcl  25148  resscdrg  25322  ishl2  25334  recms  25344  reust  25345  evthicc  25423  evthicc2  25424  ovolfsf  25435  volcn  25570  volivth  25571  ismbf  25592  cncombf  25622  cnmbf  25623  0plef  25636  itg1ge0  25650  i1faddlem  25657  i1fmul  25660  itg1addlem4  25663  i1fsub  25672  itg1sub  25673  mbfi1fseqlem5  25683  xrge0f  25695  itg20  25701  itg2const  25704  itg2mulc  25711  itg2addlem  25722  i1fibl  25772  itgitg1  25773  iblabslem  25792  iblabs  25793  bddmulibl  25803  recnprss  25868  dvmptresicc  25880  dvcjbr  25913  dvfre  25915  dvnfre  25916  dvferm1  25949  dvferm2  25951  rolle  25954  cmvth  25955  mvth  25956  dvlip  25957  dvlipcn  25958  dvlip2  25959  c1liplem1  25960  c1lip2  25962  dvgt0lem1  25966  dvle  25971  dvivthlem1  25972  dvivth  25974  dvne0  25975  lhop1lem  25977  lhop1  25978  lhop2  25979  lhop  25980  dvcnvrelem1  25981  dvcnvrelem2  25982  dvcnvre  25983  dvcvx  25984  dvfsumle  25985  dvfsumge  25986  dvfsumabs  25987  dvfsumlem2  25991  dvfsumrlim  25995  ftc1a  26001  ftc1lem3  26002  ftc1lem6  26005  ftc1  26006  ftc1cn  26007  ftc2  26008  ftc2ditglem  26009  itgparts  26011  itgsubstlem  26012  itgsubst  26013  itgpowd  26014  aacjcl  26290  aalioulem3  26297  taylthlem2  26336  taylth  26337  abelth2  26404  reeff1olem  26408  efcvx  26411  pilem3  26415  pige3ALT  26481  recosf1o  26496  resinf1o  26497  dvrelog  26598  relogcn  26599  logcnlem5  26607  logcn  26608  dvloglem  26609  dvlog2lem  26613  logccv  26624  dvcxp1  26701  cxpcn3  26709  resqrtcn  26710  loglesqrt  26722  ssscongptld  26783  ressatans  26895  rlimcnp  26926  efrlim  26930  jensenlem1  26947  jensenlem2  26948  jensen  26949  amgm  26951  lgamgulmlem2  26990  ftalem3  27035  basellem9  27049  efnnfsumcl  27063  efchtdvds  27119  lgsdchr  27315  dchrvmasumlem1  27455  dchrisum0lem3  27479  pntlem3  27569  cchhllem  28952  ex-fpar  30529  ipasslem7  30904  fprodex01  32895  indsumin  32918  rexdiv  32982  fsumrp0cl  33078  xrge0slmod  33405  ccfldsrarelvec  33812  ccfldextdgrr  33813  rmulccn  34069  raddcn  34070  xrge0iifhom  34078  lmlimxrge0  34089  rezh  34110  esumpfinvallem  34215  esumpfinval  34216  esumpfinvalf  34217  esumcvg  34227  plymulx0  34688  plymulx  34689  signsplypnf  34691  signsply0  34692  iblidicc  34733  rpsqrtcn  34734  ftc2re  34739  fdvposlt  34740  fdvneggt  34741  fdvposle  34742  fdvnegge  34743  itgexpif  34747  circlemeth  34781  circlemethnat  34782  circlevma  34783  circlemethhgt  34784  logdivsqrle  34791  resconn  35425  ivthALT  36514  dnicn  36749  knoppcnlem10  36759  knoppcnlem11  36760  unbdqndv2  36768  knoppndv  36791  knoppcn2  36793  broucube  37972  mblfinlem2  37976  mbfresfi  37984  ftc1cnnclem  38009  ftc1cnnc  38010  ftc1anclem3  38013  ftc1anclem5  38015  ftc1anclem7  38017  ftc1anclem8  38018  ftc1anc  38019  ftc2nc  38020  asindmre  38021  dvreasin  38024  dvreacos  38025  areacirclem1  38026  areacirclem2  38027  areacirclem3  38028  areacirclem4  38029  areacirc  38031  repwsmet  38152  rrnequiv  38153  rrntotbnd  38154  reheibor  38157  iccbnd  38158  intlewftc  42497  dvrelog2  42500  dvrelog3  42501  aks4d1p1p5  42511  rpsscn  42728  redvmptabs  42789  readvrec2  42790  resuppsinopn  42792  readvcot  42793  resubeqsub  42859  subresre  42860  arearect  43640  areaquad  43641  k0004val0  44578  extoimad  44588  imo72b2lem0  44589  imo72b2lem2  44591  imo72b2lem1  44593  imo72b2  44596  ssrecnpr  44732  sblpnf  44734  radcnvrat  44738  lhe4.4ex1a  44753  refsumcn  45458  rr2sscn2  45792  uzsscn  45900  evthiccabs  45923  climreeq  46040  limciccioolb  46048  limcrecl  46056  limcicciooub  46062  limcleqr  46069  lptioo2cn  46070  lptioo1cn  46071  limclner  46076  liminflimsupclim  46232  resincncf  46300  cncficcgt0  46313  cncfiooicclem1  46318  cncfiooiccre  46320  jumpncnp  46323  dvcosre  46337  dvmptconst  46340  dvmptidg  46342  fperdvper  46344  dvresioo  46346  dvmulcncf  46350  dvdivcncf  46352  dvbdfbdioolem1  46353  ioodvbdlimc1lem1  46356  ioodvbdlimc1lem2  46357  ioodvbdlimc1  46358  ioodvbdlimc2lem  46359  ioodvbdlimc2  46360  itgsin0pilem1  46375  ibliccsinexp  46376  iblioosinexp  46378  itgsinexplem1  46379  itgsinexp  46380  itgcoscmulx  46394  itgsincmulx  46399  itgsubsticclem  46400  itgiccshift  46405  itgperiod  46406  itgsbtaddcnst  46407  dirkeritg  46527  dirkercncflem2  46529  dirkercncflem3  46530  dirkercncflem4  46531  dirkercncf  46532  fourierdlem16  46548  fourierdlem18  46550  fourierdlem21  46553  fourierdlem22  46554  fourierdlem39  46571  fourierdlem42  46574  fourierdlem48  46579  fourierdlem49  46580  fourierdlem53  46584  fourierdlem57  46588  fourierdlem58  46589  fourierdlem59  46590  fourierdlem60  46591  fourierdlem61  46592  fourierdlem62  46593  fourierdlem68  46599  fourierdlem70  46601  fourierdlem72  46603  fourierdlem73  46604  fourierdlem74  46605  fourierdlem75  46606  fourierdlem76  46607  fourierdlem78  46609  fourierdlem80  46611  fourierdlem83  46614  fourierdlem84  46615  fourierdlem85  46616  fourierdlem88  46619  fourierdlem89  46620  fourierdlem90  46621  fourierdlem91  46622  fourierdlem93  46624  fourierdlem94  46625  fourierdlem95  46626  fourierdlem96  46627  fourierdlem97  46628  fourierdlem98  46629  fourierdlem99  46630  fourierdlem101  46632  fourierdlem103  46634  fourierdlem104  46635  fourierdlem111  46642  fourierdlem112  46643  fourierdlem113  46644  fouriercnp  46651  sqwvfoura  46653  sqwvfourb  46654  fouriersw  46656  fouriercn  46657  etransclem2  46661  etransclem18  46677  etransclem23  46682  etransclem46  46705  rrxtopnfi  46712  rrndistlt  46715  sge0sn  46804  sge0tsms  46805  sge0f1o  46807  sge0pr  46819  sge0resplit  46831  sge0iunmptlemre  46840  sge0isummpt2  46857  hoicvr  46973  hoidmvlelem2  47021  lamberte  47327  refdivmptf  49009  refdivmptfv  49013  amgmlemALT  50269