Axiom ax-resscn 11081

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 11023	. 2 class ℝ
2		cc 11022	. 2 class ℂ
3	1, 2	wss 3899	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  11114  reex  11115  recni  11144  qsscn  12871  ioosscn  13322  unitsscn  13414  reexpcl  13999  rpexpcl  14001  reexpclz  14003  expge0  14019  expge1  14020  rlimrecl  15501  abscn2  15520  recn2  15522  imcn2  15523  climabs  15525  climre  15527  climim  15528  rlimabs  15530  rlimre  15532  rlimim  15533  caurcvgr  15595  caucvgrlem2  15596  caurcvg  15598  fsumrecl  15655  fsumrpcl  15658  fsumge0  15716  fsumre  15729  fsumim  15730  fprodrecl  15874  fprodrpcl  15877  fprodreclf  15880  fprodge0  15914  fprodge1  15916  rerisefaccl  15938  refallfaccl  15939  rprisefaccl  15944  reeff1  16043  nthruc  16175  regsumfsum  21388  rge0srg  21391  rebase  21559  re0g  21565  regsumsupp  21575  remet  24732  tgioo2  24745  xrsdsre  24753  recld2  24757  reperf  24762  iitopon  24826  dfii3  24830  abscncf  24848  recncf  24849  imcncf  24850  abscncfALT  24872  cnmptre  24875  iimulcnOLD  24889  icchmeo  24892  icchmeoOLD  24893  cnrehmeo  24905  cnrehmeoOLD  24906  evth  24912  evth2  24913  lebnumlem2  24915  lebnumii  24919  reparphtiOLD  24951  cphsqrtcl  25138  resscdrg  25312  ishl2  25324  recms  25334  reust  25335  evthicc  25414  evthicc2  25415  ovolfsf  25426  volcn  25561  volivth  25562  ismbf  25583  cncombf  25613  cnmbf  25614  0plef  25627  itg1ge0  25641  i1faddlem  25648  i1fmul  25651  itg1addlem4  25654  i1fsub  25663  itg1sub  25664  mbfi1fseqlem5  25674  xrge0f  25686  itg20  25692  itg2const  25695  itg2mulc  25702  itg2addlem  25713  i1fibl  25763  itgitg1  25764  iblabslem  25783  iblabs  25784  bddmulibl  25794  recnprss  25859  dvmptresicc  25871  dvcjbr  25907  dvfre  25909  dvnfre  25910  dvferm1  25943  dvferm2  25945  rolle  25948  cmvth  25949  cmvthOLD  25950  mvth  25951  dvlip  25952  dvlipcn  25953  dvlip2  25954  c1liplem1  25955  c1lip2  25957  dvgt0lem1  25961  dvle  25966  dvivthlem1  25967  dvivth  25969  dvne0  25970  lhop1lem  25972  lhop1  25973  lhop2  25974  lhop  25975  dvcnvrelem1  25976  dvcnvrelem2  25977  dvcnvre  25978  dvcvx  25979  dvfsumle  25980  dvfsumleOLD  25981  dvfsumge  25982  dvfsumabs  25983  dvfsumlem2  25987  dvfsumlem2OLD  25988  dvfsumrlim  25992  ftc1a  25998  ftc1lem3  25999  ftc1lem6  26002  ftc1  26003  ftc1cn  26004  ftc2  26005  ftc2ditglem  26006  itgparts  26008  itgsubstlem  26009  itgsubst  26010  itgpowd  26011  aacjcl  26289  aalioulem3  26296  taylthlem2  26336  taylthlem2OLD  26337  taylth  26338  abelth2  26406  reeff1olem  26410  efcvx  26413  pilem3  26417  pige3ALT  26483  recosf1o  26498  resinf1o  26499  dvrelog  26600  relogcn  26601  logcnlem5  26609  logcn  26610  dvloglem  26611  dvlog2lem  26615  logccv  26626  dvcxp1  26703  cxpcn3  26712  resqrtcn  26713  loglesqrt  26725  ssscongptld  26786  ressatans  26898  rlimcnp  26929  efrlim  26933  efrlimOLD  26934  jensenlem1  26951  jensenlem2  26952  jensen  26953  amgm  26955  lgamgulmlem2  26994  ftalem3  27039  basellem9  27053  efnnfsumcl  27067  efchtdvds  27123  lgsdchr  27320  dchrvmasumlem1  27460  dchrisum0lem3  27484  pntlem3  27574  cchhllem  28908  ex-fpar  30486  ipasslem7  30860  fprodex01  32855  indsumin  32892  rexdiv  32956  fsumrp0cl  33052  xrge0slmod  33378  ccfldsrarelvec  33777  ccfldextdgrr  33778  rmulccn  34034  raddcn  34035  xrge0iifhom  34043  lmlimxrge0  34054  rezh  34075  esumpfinvallem  34180  esumpfinval  34181  esumpfinvalf  34182  esumcvg  34192  plymulx0  34653  plymulx  34654  signsplypnf  34656  signsply0  34657  iblidicc  34698  rpsqrtcn  34699  ftc2re  34704  fdvposlt  34705  fdvneggt  34706  fdvposle  34707  fdvnegge  34708  itgexpif  34712  circlemeth  34746  circlemethnat  34747  circlevma  34748  circlemethhgt  34749  logdivsqrle  34756  resconn  35389  ivthALT  36478  dnicn  36635  knoppcnlem10  36645  knoppcnlem11  36646  unbdqndv2  36654  knoppndv  36677  knoppcn2  36679  broucube  37794  mblfinlem2  37798  mbfresfi  37806  ftc1cnnclem  37831  ftc1cnnc  37832  ftc1anclem3  37835  ftc1anclem5  37837  ftc1anclem7  37839  ftc1anclem8  37840  ftc1anc  37841  ftc2nc  37842  asindmre  37843  dvreasin  37846  dvreacos  37847  areacirclem1  37848  areacirclem2  37849  areacirclem3  37850  areacirclem4  37851  areacirc  37853  repwsmet  37974  rrnequiv  37975  rrntotbnd  37976  reheibor  37979  iccbnd  37980  intlewftc  42254  dvrelog2  42257  dvrelog3  42258  aks4d1p1p5  42268  rpsscn  42496  redvmptabs  42557  readvrec2  42558  resuppsinopn  42560  readvcot  42561  resubeqsub  42627  subresre  42628  arearect  43399  areaquad  43400  k0004val0  44337  extoimad  44347  imo72b2lem0  44348  imo72b2lem2  44350  imo72b2lem1  44352  imo72b2  44355  ssrecnpr  44491  sblpnf  44493  radcnvrat  44497  lhe4.4ex1a  44512  refsumcn  45217  rr2sscn2  45552  uzsscn  45661  evthiccabs  45684  climreeq  45801  limciccioolb  45809  limcrecl  45817  limcicciooub  45823  limcleqr  45830  lptioo2cn  45831  lptioo1cn  45832  limclner  45837  liminflimsupclim  45993  resincncf  46061  cncficcgt0  46074  cncfiooicclem1  46079  cncfiooiccre  46081  jumpncnp  46084  dvcosre  46098  dvmptconst  46101  dvmptidg  46103  fperdvper  46105  dvresioo  46107  dvmulcncf  46111  dvdivcncf  46113  dvbdfbdioolem1  46114  ioodvbdlimc1lem1  46117  ioodvbdlimc1lem2  46118  ioodvbdlimc1  46119  ioodvbdlimc2lem  46120  ioodvbdlimc2  46121  itgsin0pilem1  46136  ibliccsinexp  46137  iblioosinexp  46139  itgsinexplem1  46140  itgsinexp  46141  itgcoscmulx  46155  itgsincmulx  46160  itgsubsticclem  46161  itgiccshift  46166  itgperiod  46167  itgsbtaddcnst  46168  dirkeritg  46288  dirkercncflem2  46290  dirkercncflem3  46291  dirkercncflem4  46292  dirkercncf  46293  fourierdlem16  46309  fourierdlem18  46311  fourierdlem21  46314  fourierdlem22  46315  fourierdlem39  46332  fourierdlem42  46335  fourierdlem48  46340  fourierdlem49  46341  fourierdlem53  46345  fourierdlem57  46349  fourierdlem58  46350  fourierdlem59  46351  fourierdlem60  46352  fourierdlem61  46353  fourierdlem62  46354  fourierdlem68  46360  fourierdlem70  46362  fourierdlem72  46364  fourierdlem73  46365  fourierdlem74  46366  fourierdlem75  46367  fourierdlem76  46368  fourierdlem78  46370  fourierdlem80  46372  fourierdlem83  46375  fourierdlem84  46376  fourierdlem85  46377  fourierdlem88  46380  fourierdlem89  46381  fourierdlem90  46382  fourierdlem91  46383  fourierdlem93  46385  fourierdlem94  46386  fourierdlem95  46387  fourierdlem96  46388  fourierdlem97  46389  fourierdlem98  46390  fourierdlem99  46391  fourierdlem101  46393  fourierdlem103  46395  fourierdlem104  46396  fourierdlem111  46403  fourierdlem112  46404  fourierdlem113  46405  fouriercnp  46412  sqwvfoura  46414  sqwvfourb  46415  fouriersw  46417  fouriercn  46418  etransclem2  46422  etransclem18  46438  etransclem23  46443  etransclem46  46466  rrxtopnfi  46473  rrndistlt  46476  sge0sn  46565  sge0tsms  46566  sge0f1o  46568  sge0pr  46580  sge0resplit  46592  sge0iunmptlemre  46601  sge0isummpt2  46618  hoicvr  46734  hoidmvlelem2  46782  lamberte  47076  refdivmptf  48730  refdivmptfv  48734  amgmlemALT  49990