Axiom ax-resscn 11212

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 11154	. 2 class ℝ
2		cc 11153	. 2 class ℂ
3	1, 2	wss 3951	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  11245  reex  11246  recni  11275  qsscn  13002  ioosscn  13449  unitsscn  13540  reexpcl  14119  rpexpcl  14121  reexpclz  14123  expge0  14139  expge1  14140  rlimrecl  15616  abscn2  15635  recn2  15637  imcn2  15638  climabs  15640  climre  15642  climim  15643  rlimabs  15645  rlimre  15647  rlimim  15648  caurcvgr  15710  caucvgrlem2  15711  caurcvg  15713  fsumrecl  15770  fsumrpcl  15773  fsumge0  15831  fsumre  15844  fsumim  15845  fprodrecl  15989  fprodrpcl  15992  fprodreclf  15995  fprodge0  16029  fprodge1  16031  rerisefaccl  16053  refallfaccl  16054  rprisefaccl  16059  reeff1  16156  nthruc  16288  regsumfsum  21453  rge0srg  21456  rebase  21624  re0g  21630  regsumsupp  21640  remet  24811  tgioo2  24824  xrsdsre  24832  recld2  24836  reperf  24841  iitopon  24905  dfii3  24909  abscncf  24927  recncf  24928  imcncf  24929  abscncfALT  24951  cnmptre  24954  iimulcnOLD  24968  icchmeo  24971  icchmeoOLD  24972  cnrehmeo  24984  cnrehmeoOLD  24985  evth  24991  evth2  24992  lebnumlem2  24994  lebnumii  24998  reparphtiOLD  25030  cphsqrtcl  25218  resscdrg  25392  ishl2  25404  recms  25414  reust  25415  evthicc  25494  evthicc2  25495  ovolfsf  25506  volcn  25641  volivth  25642  ismbf  25663  cncombf  25693  cnmbf  25694  0plef  25707  itg1ge0  25721  i1faddlem  25728  i1fmul  25731  itg1addlem4  25734  i1fsub  25743  itg1sub  25744  mbfi1fseqlem5  25754  xrge0f  25766  itg20  25772  itg2const  25775  itg2mulc  25782  itg2addlem  25793  i1fibl  25843  itgitg1  25844  iblabslem  25863  iblabs  25864  bddmulibl  25874  recnprss  25939  dvmptresicc  25951  dvcjbr  25987  dvfre  25989  dvnfre  25990  dvferm1  26023  dvferm2  26025  rolle  26028  cmvth  26029  cmvthOLD  26030  mvth  26031  dvlip  26032  dvlipcn  26033  dvlip2  26034  c1liplem1  26035  c1lip2  26037  dvgt0lem1  26041  dvle  26046  dvivthlem1  26047  dvivth  26049  dvne0  26050  lhop1lem  26052  lhop1  26053  lhop2  26054  lhop  26055  dvcnvrelem1  26056  dvcnvrelem2  26057  dvcnvre  26058  dvcvx  26059  dvfsumle  26060  dvfsumleOLD  26061  dvfsumge  26062  dvfsumabs  26063  dvfsumlem2  26067  dvfsumlem2OLD  26068  dvfsumrlim  26072  ftc1a  26078  ftc1lem3  26079  ftc1lem6  26082  ftc1  26083  ftc1cn  26084  ftc2  26085  ftc2ditglem  26086  itgparts  26088  itgsubstlem  26089  itgsubst  26090  itgpowd  26091  aacjcl  26369  aalioulem3  26376  taylthlem2  26416  taylthlem2OLD  26417  taylth  26418  abelth2  26486  reeff1olem  26490  efcvx  26493  pilem3  26497  pige3ALT  26562  recosf1o  26577  resinf1o  26578  dvrelog  26679  relogcn  26680  logcnlem5  26688  logcn  26689  dvloglem  26690  dvlog2lem  26694  logccv  26705  dvcxp1  26782  cxpcn3  26791  resqrtcn  26792  loglesqrt  26804  ssscongptld  26865  ressatans  26977  rlimcnp  27008  efrlim  27012  efrlimOLD  27013  jensenlem1  27030  jensenlem2  27031  jensen  27032  amgm  27034  lgamgulmlem2  27073  ftalem3  27118  basellem9  27132  efnnfsumcl  27146  efchtdvds  27202  lgsdchr  27399  dchrvmasumlem1  27539  dchrisum0lem3  27563  pntlem3  27653  cchhllem  28901  cchhllemOLD  28902  ex-fpar  30481  ipasslem7  30855  fprodex01  32827  indsumin  32847  rexdiv  32908  fsumrp0cl  33026  xrge0slmod  33376  ccfldsrarelvec  33721  ccfldextdgrr  33722  rmulccn  33927  raddcn  33928  xrge0iifhom  33936  lmlimxrge0  33947  rezh  33970  esumpfinvallem  34075  esumpfinval  34076  esumpfinvalf  34077  esumcvg  34087  plymulx0  34562  plymulx  34563  signsplypnf  34565  signsply0  34566  iblidicc  34607  rpsqrtcn  34608  ftc2re  34613  fdvposlt  34614  fdvneggt  34615  fdvposle  34616  fdvnegge  34617  itgexpif  34621  circlemeth  34655  circlemethnat  34656  circlevma  34657  circlemethhgt  34658  logdivsqrle  34665  resconn  35251  ivthALT  36336  dnicn  36493  knoppcnlem10  36503  knoppcnlem11  36504  unbdqndv2  36512  knoppndv  36535  knoppcn2  36537  broucube  37661  mblfinlem2  37665  mbfresfi  37673  ftc1cnnclem  37698  ftc1cnnc  37699  ftc1anclem3  37702  ftc1anclem5  37704  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708  ftc2nc  37709  asindmre  37710  dvreasin  37713  dvreacos  37714  areacirclem1  37715  areacirclem2  37716  areacirclem3  37717  areacirclem4  37718  areacirc  37720  repwsmet  37841  rrnequiv  37842  rrntotbnd  37843  reheibor  37846  iccbnd  37847  intlewftc  42062  dvrelog2  42065  dvrelog3  42066  aks4d1p1p5  42076  rpsscn  42333  redvmptabs  42390  readvrec2  42391  resuppsinopn  42393  readvcot  42394  resubeqsub  42459  subresre  42460  arearect  43227  areaquad  43228  k0004val0  44167  extoimad  44177  imo72b2lem0  44178  imo72b2lem2  44180  imo72b2lem1  44182  imo72b2  44185  ssrecnpr  44327  sblpnf  44329  radcnvrat  44333  lhe4.4ex1a  44348  refsumcn  45035  rr2sscn2  45377  uzsscn  45486  evthiccabs  45509  climreeq  45628  limciccioolb  45636  limcrecl  45644  limcicciooub  45652  limcleqr  45659  lptioo2cn  45660  lptioo1cn  45661  limclner  45666  liminflimsupclim  45822  resincncf  45890  cncficcgt0  45903  cncfiooicclem1  45908  cncfiooiccre  45910  jumpncnp  45913  dvcosre  45927  dvmptconst  45930  dvmptidg  45932  fperdvper  45934  dvresioo  45936  dvmulcncf  45940  dvdivcncf  45942  dvbdfbdioolem1  45943  ioodvbdlimc1lem1  45946  ioodvbdlimc1lem2  45947  ioodvbdlimc1  45948  ioodvbdlimc2lem  45949  ioodvbdlimc2  45950  itgsin0pilem1  45965  ibliccsinexp  45966  iblioosinexp  45968  itgsinexplem1  45969  itgsinexp  45970  itgcoscmulx  45984  itgsincmulx  45989  itgsubsticclem  45990  itgiccshift  45995  itgperiod  45996  itgsbtaddcnst  45997  dirkeritg  46117  dirkercncflem2  46119  dirkercncflem3  46120  dirkercncflem4  46121  dirkercncf  46122  fourierdlem16  46138  fourierdlem18  46140  fourierdlem21  46143  fourierdlem22  46144  fourierdlem39  46161  fourierdlem42  46164  fourierdlem48  46169  fourierdlem49  46170  fourierdlem53  46174  fourierdlem57  46178  fourierdlem58  46179  fourierdlem59  46180  fourierdlem60  46181  fourierdlem61  46182  fourierdlem62  46183  fourierdlem68  46189  fourierdlem70  46191  fourierdlem72  46193  fourierdlem73  46194  fourierdlem74  46195  fourierdlem75  46196  fourierdlem76  46197  fourierdlem78  46199  fourierdlem80  46201  fourierdlem83  46204  fourierdlem84  46205  fourierdlem85  46206  fourierdlem88  46209  fourierdlem89  46210  fourierdlem90  46211  fourierdlem91  46212  fourierdlem93  46214  fourierdlem94  46215  fourierdlem95  46216  fourierdlem96  46217  fourierdlem97  46218  fourierdlem98  46219  fourierdlem99  46220  fourierdlem101  46222  fourierdlem103  46224  fourierdlem104  46225  fourierdlem111  46232  fourierdlem112  46233  fourierdlem113  46234  fouriercnp  46241  sqwvfoura  46243  sqwvfourb  46244  fouriersw  46246  fouriercn  46247  etransclem2  46251  etransclem18  46267  etransclem23  46272  etransclem46  46295  rrxtopnfi  46302  rrndistlt  46305  sge0sn  46394  sge0tsms  46395  sge0f1o  46397  sge0pr  46409  sge0resplit  46421  sge0iunmptlemre  46430  sge0isummpt2  46447  hoicvr  46563  hoidmvlelem2  46611  refdivmptf  48463  refdivmptfv  48467  amgmlemALT  49322