Axiom ax-resscn 11087

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 11029	. 2 class ℝ
2		cc 11028	. 2 class ℂ
3	1, 2	wss 3902	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  11120  reex  11121  recni  11150  qsscn  12877  ioosscn  13328  unitsscn  13420  reexpcl  14005  rpexpcl  14007  reexpclz  14009  expge0  14025  expge1  14026  rlimrecl  15507  abscn2  15526  recn2  15528  imcn2  15529  climabs  15531  climre  15533  climim  15534  rlimabs  15536  rlimre  15538  rlimim  15539  caurcvgr  15601  caucvgrlem2  15602  caurcvg  15604  fsumrecl  15661  fsumrpcl  15664  fsumge0  15722  fsumre  15735  fsumim  15736  fprodrecl  15880  fprodrpcl  15883  fprodreclf  15886  fprodge0  15920  fprodge1  15922  rerisefaccl  15944  refallfaccl  15945  rprisefaccl  15950  reeff1  16049  nthruc  16181  regsumfsum  21394  rge0srg  21397  rebase  21565  re0g  21571  regsumsupp  21581  remet  24738  tgioo2  24751  xrsdsre  24759  recld2  24763  reperf  24768  iitopon  24832  dfii3  24836  abscncf  24854  recncf  24855  imcncf  24856  abscncfALT  24878  cnmptre  24881  iimulcnOLD  24895  icchmeo  24898  icchmeoOLD  24899  cnrehmeo  24911  cnrehmeoOLD  24912  evth  24918  evth2  24919  lebnumlem2  24921  lebnumii  24925  reparphtiOLD  24957  cphsqrtcl  25144  resscdrg  25318  ishl2  25330  recms  25340  reust  25341  evthicc  25420  evthicc2  25421  ovolfsf  25432  volcn  25567  volivth  25568  ismbf  25589  cncombf  25619  cnmbf  25620  0plef  25633  itg1ge0  25647  i1faddlem  25654  i1fmul  25657  itg1addlem4  25660  i1fsub  25669  itg1sub  25670  mbfi1fseqlem5  25680  xrge0f  25692  itg20  25698  itg2const  25701  itg2mulc  25708  itg2addlem  25719  i1fibl  25769  itgitg1  25770  iblabslem  25789  iblabs  25790  bddmulibl  25800  recnprss  25865  dvmptresicc  25877  dvcjbr  25913  dvfre  25915  dvnfre  25916  dvferm1  25949  dvferm2  25951  rolle  25954  cmvth  25955  cmvthOLD  25956  mvth  25957  dvlip  25958  dvlipcn  25959  dvlip2  25960  c1liplem1  25961  c1lip2  25963  dvgt0lem1  25967  dvle  25972  dvivthlem1  25973  dvivth  25975  dvne0  25976  lhop1lem  25978  lhop1  25979  lhop2  25980  lhop  25981  dvcnvrelem1  25982  dvcnvrelem2  25983  dvcnvre  25984  dvcvx  25985  dvfsumle  25986  dvfsumleOLD  25987  dvfsumge  25988  dvfsumabs  25989  dvfsumlem2  25993  dvfsumlem2OLD  25994  dvfsumrlim  25998  ftc1a  26004  ftc1lem3  26005  ftc1lem6  26008  ftc1  26009  ftc1cn  26010  ftc2  26011  ftc2ditglem  26012  itgparts  26014  itgsubstlem  26015  itgsubst  26016  itgpowd  26017  aacjcl  26295  aalioulem3  26302  taylthlem2  26342  taylthlem2OLD  26343  taylth  26344  abelth2  26412  reeff1olem  26416  efcvx  26419  pilem3  26423  pige3ALT  26489  recosf1o  26504  resinf1o  26505  dvrelog  26606  relogcn  26607  logcnlem5  26615  logcn  26616  dvloglem  26617  dvlog2lem  26621  logccv  26632  dvcxp1  26709  cxpcn3  26718  resqrtcn  26719  loglesqrt  26731  ssscongptld  26792  ressatans  26904  rlimcnp  26935  efrlim  26939  efrlimOLD  26940  jensenlem1  26957  jensenlem2  26958  jensen  26959  amgm  26961  lgamgulmlem2  27000  ftalem3  27045  basellem9  27059  efnnfsumcl  27073  efchtdvds  27129  lgsdchr  27326  dchrvmasumlem1  27466  dchrisum0lem3  27490  pntlem3  27580  cchhllem  28963  ex-fpar  30541  ipasslem7  30915  fprodex01  32908  indsumin  32945  rexdiv  33009  fsumrp0cl  33105  xrge0slmod  33431  ccfldsrarelvec  33830  ccfldextdgrr  33831  rmulccn  34087  raddcn  34088  xrge0iifhom  34096  lmlimxrge0  34107  rezh  34128  esumpfinvallem  34233  esumpfinval  34234  esumpfinvalf  34235  esumcvg  34245  plymulx0  34706  plymulx  34707  signsplypnf  34709  signsply0  34710  iblidicc  34751  rpsqrtcn  34752  ftc2re  34757  fdvposlt  34758  fdvneggt  34759  fdvposle  34760  fdvnegge  34761  itgexpif  34765  circlemeth  34799  circlemethnat  34800  circlevma  34801  circlemethhgt  34802  logdivsqrle  34809  resconn  35442  ivthALT  36531  dnicn  36694  knoppcnlem10  36704  knoppcnlem11  36705  unbdqndv2  36713  knoppndv  36736  knoppcn2  36738  broucube  37857  mblfinlem2  37861  mbfresfi  37869  ftc1cnnclem  37894  ftc1cnnc  37895  ftc1anclem3  37898  ftc1anclem5  37900  ftc1anclem7  37902  ftc1anclem8  37903  ftc1anc  37904  ftc2nc  37905  asindmre  37906  dvreasin  37909  dvreacos  37910  areacirclem1  37911  areacirclem2  37912  areacirclem3  37913  areacirclem4  37914  areacirc  37916  repwsmet  38037  rrnequiv  38038  rrntotbnd  38039  reheibor  38042  iccbnd  38043  intlewftc  42383  dvrelog2  42386  dvrelog3  42387  aks4d1p1p5  42397  rpsscn  42621  redvmptabs  42682  readvrec2  42683  resuppsinopn  42685  readvcot  42686  resubeqsub  42752  subresre  42753  arearect  43524  areaquad  43525  k0004val0  44462  extoimad  44472  imo72b2lem0  44473  imo72b2lem2  44475  imo72b2lem1  44477  imo72b2  44480  ssrecnpr  44616  sblpnf  44618  radcnvrat  44622  lhe4.4ex1a  44637  refsumcn  45342  rr2sscn2  45677  uzsscn  45786  evthiccabs  45809  climreeq  45926  limciccioolb  45934  limcrecl  45942  limcicciooub  45948  limcleqr  45955  lptioo2cn  45956  lptioo1cn  45957  limclner  45962  liminflimsupclim  46118  resincncf  46186  cncficcgt0  46199  cncfiooicclem1  46204  cncfiooiccre  46206  jumpncnp  46209  dvcosre  46223  dvmptconst  46226  dvmptidg  46228  fperdvper  46230  dvresioo  46232  dvmulcncf  46236  dvdivcncf  46238  dvbdfbdioolem1  46239  ioodvbdlimc1lem1  46242  ioodvbdlimc1lem2  46243  ioodvbdlimc1  46244  ioodvbdlimc2lem  46245  ioodvbdlimc2  46246  itgsin0pilem1  46261  ibliccsinexp  46262  iblioosinexp  46264  itgsinexplem1  46265  itgsinexp  46266  itgcoscmulx  46280  itgsincmulx  46285  itgsubsticclem  46286  itgiccshift  46291  itgperiod  46292  itgsbtaddcnst  46293  dirkeritg  46413  dirkercncflem2  46415  dirkercncflem3  46416  dirkercncflem4  46417  dirkercncf  46418  fourierdlem16  46434  fourierdlem18  46436  fourierdlem21  46439  fourierdlem22  46440  fourierdlem39  46457  fourierdlem42  46460  fourierdlem48  46465  fourierdlem49  46466  fourierdlem53  46470  fourierdlem57  46474  fourierdlem58  46475  fourierdlem59  46476  fourierdlem60  46477  fourierdlem61  46478  fourierdlem62  46479  fourierdlem68  46485  fourierdlem70  46487  fourierdlem72  46489  fourierdlem73  46490  fourierdlem74  46491  fourierdlem75  46492  fourierdlem76  46493  fourierdlem78  46495  fourierdlem80  46497  fourierdlem83  46500  fourierdlem84  46501  fourierdlem85  46502  fourierdlem88  46505  fourierdlem89  46506  fourierdlem90  46507  fourierdlem91  46508  fourierdlem93  46510  fourierdlem94  46511  fourierdlem95  46512  fourierdlem96  46513  fourierdlem97  46514  fourierdlem98  46515  fourierdlem99  46516  fourierdlem101  46518  fourierdlem103  46520  fourierdlem104  46521  fourierdlem111  46528  fourierdlem112  46529  fourierdlem113  46530  fouriercnp  46537  sqwvfoura  46539  sqwvfourb  46540  fouriersw  46542  fouriercn  46543  etransclem2  46547  etransclem18  46563  etransclem23  46568  etransclem46  46591  rrxtopnfi  46598  rrndistlt  46601  sge0sn  46690  sge0tsms  46691  sge0f1o  46693  sge0pr  46705  sge0resplit  46717  sge0iunmptlemre  46726  sge0isummpt2  46743  hoicvr  46859  hoidmvlelem2  46907  lamberte  47201  refdivmptf  48855  refdivmptfv  48859  amgmlemALT  50115