Axiom ax-resscn 11125

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 11067	. 2 class ℝ
2		cc 11066	. 2 class ℂ
3	1, 2	wss 3914	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  11158  reex  11159  recni  11188  qsscn  12919  ioosscn  13369  unitsscn  13461  reexpcl  14043  rpexpcl  14045  reexpclz  14047  expge0  14063  expge1  14064  rlimrecl  15546  abscn2  15565  recn2  15567  imcn2  15568  climabs  15570  climre  15572  climim  15573  rlimabs  15575  rlimre  15577  rlimim  15578  caurcvgr  15640  caucvgrlem2  15641  caurcvg  15643  fsumrecl  15700  fsumrpcl  15703  fsumge0  15761  fsumre  15774  fsumim  15775  fprodrecl  15919  fprodrpcl  15922  fprodreclf  15925  fprodge0  15959  fprodge1  15961  rerisefaccl  15983  refallfaccl  15984  rprisefaccl  15989  reeff1  16088  nthruc  16220  regsumfsum  21352  rge0srg  21355  rebase  21515  re0g  21521  regsumsupp  21531  remet  24678  tgioo2  24691  xrsdsre  24699  recld2  24703  reperf  24708  iitopon  24772  dfii3  24776  abscncf  24794  recncf  24795  imcncf  24796  abscncfALT  24818  cnmptre  24821  iimulcnOLD  24835  icchmeo  24838  icchmeoOLD  24839  cnrehmeo  24851  cnrehmeoOLD  24852  evth  24858  evth2  24859  lebnumlem2  24861  lebnumii  24865  reparphtiOLD  24897  cphsqrtcl  25084  resscdrg  25258  ishl2  25270  recms  25280  reust  25281  evthicc  25360  evthicc2  25361  ovolfsf  25372  volcn  25507  volivth  25508  ismbf  25529  cncombf  25559  cnmbf  25560  0plef  25573  itg1ge0  25587  i1faddlem  25594  i1fmul  25597  itg1addlem4  25600  i1fsub  25609  itg1sub  25610  mbfi1fseqlem5  25620  xrge0f  25632  itg20  25638  itg2const  25641  itg2mulc  25648  itg2addlem  25659  i1fibl  25709  itgitg1  25710  iblabslem  25729  iblabs  25730  bddmulibl  25740  recnprss  25805  dvmptresicc  25817  dvcjbr  25853  dvfre  25855  dvnfre  25856  dvferm1  25889  dvferm2  25891  rolle  25894  cmvth  25895  cmvthOLD  25896  mvth  25897  dvlip  25898  dvlipcn  25899  dvlip2  25900  c1liplem1  25901  c1lip2  25903  dvgt0lem1  25907  dvle  25912  dvivthlem1  25913  dvivth  25915  dvne0  25916  lhop1lem  25918  lhop1  25919  lhop2  25920  lhop  25921  dvcnvrelem1  25922  dvcnvrelem2  25923  dvcnvre  25924  dvcvx  25925  dvfsumle  25926  dvfsumleOLD  25927  dvfsumge  25928  dvfsumabs  25929  dvfsumlem2  25933  dvfsumlem2OLD  25934  dvfsumrlim  25938  ftc1a  25944  ftc1lem3  25945  ftc1lem6  25948  ftc1  25949  ftc1cn  25950  ftc2  25951  ftc2ditglem  25952  itgparts  25954  itgsubstlem  25955  itgsubst  25956  itgpowd  25957  aacjcl  26235  aalioulem3  26242  taylthlem2  26282  taylthlem2OLD  26283  taylth  26284  abelth2  26352  reeff1olem  26356  efcvx  26359  pilem3  26363  pige3ALT  26429  recosf1o  26444  resinf1o  26445  dvrelog  26546  relogcn  26547  logcnlem5  26555  logcn  26556  dvloglem  26557  dvlog2lem  26561  logccv  26572  dvcxp1  26649  cxpcn3  26658  resqrtcn  26659  loglesqrt  26671  ssscongptld  26732  ressatans  26844  rlimcnp  26875  efrlim  26879  efrlimOLD  26880  jensenlem1  26897  jensenlem2  26898  jensen  26899  amgm  26901  lgamgulmlem2  26940  ftalem3  26985  basellem9  26999  efnnfsumcl  27013  efchtdvds  27069  lgsdchr  27266  dchrvmasumlem1  27406  dchrisum0lem3  27430  pntlem3  27520  cchhllem  28814  ex-fpar  30391  ipasslem7  30765  fprodex01  32750  indsumin  32785  rexdiv  32846  fsumrp0cl  32962  xrge0slmod  33319  ccfldsrarelvec  33666  ccfldextdgrr  33667  rmulccn  33918  raddcn  33919  xrge0iifhom  33927  lmlimxrge0  33938  rezh  33959  esumpfinvallem  34064  esumpfinval  34065  esumpfinvalf  34066  esumcvg  34076  plymulx0  34538  plymulx  34539  signsplypnf  34541  signsply0  34542  iblidicc  34583  rpsqrtcn  34584  ftc2re  34589  fdvposlt  34590  fdvneggt  34591  fdvposle  34592  fdvnegge  34593  itgexpif  34597  circlemeth  34631  circlemethnat  34632  circlevma  34633  circlemethhgt  34634  logdivsqrle  34641  resconn  35233  ivthALT  36323  dnicn  36480  knoppcnlem10  36490  knoppcnlem11  36491  unbdqndv2  36499  knoppndv  36522  knoppcn2  36524  broucube  37648  mblfinlem2  37652  mbfresfi  37660  ftc1cnnclem  37685  ftc1cnnc  37686  ftc1anclem3  37689  ftc1anclem5  37691  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  ftc2nc  37696  asindmre  37697  dvreasin  37700  dvreacos  37701  areacirclem1  37702  areacirclem2  37703  areacirclem3  37704  areacirclem4  37705  areacirc  37707  repwsmet  37828  rrnequiv  37829  rrntotbnd  37830  reheibor  37833  iccbnd  37834  intlewftc  42049  dvrelog2  42052  dvrelog3  42053  aks4d1p1p5  42063  rpsscn  42287  redvmptabs  42348  readvrec2  42349  resuppsinopn  42351  readvcot  42352  resubeqsub  42418  subresre  42419  arearect  43204  areaquad  43205  k0004val0  44143  extoimad  44153  imo72b2lem0  44154  imo72b2lem2  44156  imo72b2lem1  44158  imo72b2  44161  ssrecnpr  44297  sblpnf  44299  radcnvrat  44303  lhe4.4ex1a  44318  refsumcn  45024  rr2sscn2  45362  uzsscn  45471  evthiccabs  45494  climreeq  45611  limciccioolb  45619  limcrecl  45627  limcicciooub  45635  limcleqr  45642  lptioo2cn  45643  lptioo1cn  45644  limclner  45649  liminflimsupclim  45805  resincncf  45873  cncficcgt0  45886  cncfiooicclem1  45891  cncfiooiccre  45893  jumpncnp  45896  dvcosre  45910  dvmptconst  45913  dvmptidg  45915  fperdvper  45917  dvresioo  45919  dvmulcncf  45923  dvdivcncf  45925  dvbdfbdioolem1  45926  ioodvbdlimc1lem1  45929  ioodvbdlimc1lem2  45930  ioodvbdlimc1  45931  ioodvbdlimc2lem  45932  ioodvbdlimc2  45933  itgsin0pilem1  45948  ibliccsinexp  45949  iblioosinexp  45951  itgsinexplem1  45952  itgsinexp  45953  itgcoscmulx  45967  itgsincmulx  45972  itgsubsticclem  45973  itgiccshift  45978  itgperiod  45979  itgsbtaddcnst  45980  dirkeritg  46100  dirkercncflem2  46102  dirkercncflem3  46103  dirkercncflem4  46104  dirkercncf  46105  fourierdlem16  46121  fourierdlem18  46123  fourierdlem21  46126  fourierdlem22  46127  fourierdlem39  46144  fourierdlem42  46147  fourierdlem48  46152  fourierdlem49  46153  fourierdlem53  46157  fourierdlem57  46161  fourierdlem58  46162  fourierdlem59  46163  fourierdlem60  46164  fourierdlem61  46165  fourierdlem62  46166  fourierdlem68  46172  fourierdlem70  46174  fourierdlem72  46176  fourierdlem73  46177  fourierdlem74  46178  fourierdlem75  46179  fourierdlem76  46180  fourierdlem78  46182  fourierdlem80  46184  fourierdlem83  46187  fourierdlem84  46188  fourierdlem85  46189  fourierdlem88  46192  fourierdlem89  46193  fourierdlem90  46194  fourierdlem91  46195  fourierdlem93  46197  fourierdlem94  46198  fourierdlem95  46199  fourierdlem96  46200  fourierdlem97  46201  fourierdlem98  46202  fourierdlem99  46203  fourierdlem101  46205  fourierdlem103  46207  fourierdlem104  46208  fourierdlem111  46215  fourierdlem112  46216  fourierdlem113  46217  fouriercnp  46224  sqwvfoura  46226  sqwvfourb  46227  fouriersw  46229  fouriercn  46230  etransclem2  46234  etransclem18  46250  etransclem23  46255  etransclem46  46278  rrxtopnfi  46285  rrndistlt  46288  sge0sn  46377  sge0tsms  46378  sge0f1o  46380  sge0pr  46392  sge0resplit  46404  sge0iunmptlemre  46413  sge0isummpt2  46430  hoicvr  46546  hoidmvlelem2  46594  lamberte  46889  refdivmptf  48531  refdivmptfv  48535  amgmlemALT  49792