Axiom ax-resscn 11241

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 11183	. 2 class ℝ
2		cc 11182	. 2 class ℂ
3	1, 2	wss 3976	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  11274  reex  11275  recni  11304  qsscn  13025  ioosscn  13469  unitsscn  13560  reexpcl  14129  rpexpcl  14131  reexpclz  14133  expge0  14149  expge1  14150  rlimrecl  15626  abscn2  15645  recn2  15647  imcn2  15648  climabs  15650  climre  15652  climim  15653  rlimabs  15655  rlimre  15657  rlimim  15658  caurcvgr  15722  caucvgrlem2  15723  caurcvg  15725  fsumrecl  15782  fsumrpcl  15785  fsumge0  15843  fsumre  15856  fsumim  15857  fprodrecl  16001  fprodrpcl  16004  fprodreclf  16007  fprodge0  16041  fprodge1  16043  rerisefaccl  16065  refallfaccl  16066  rprisefaccl  16071  reeff1  16168  nthruc  16300  regsumfsum  21476  rge0srg  21479  rebase  21647  re0g  21653  regsumsupp  21663  remet  24831  tgioo2  24844  xrsdsre  24851  recld2  24855  reperf  24860  iitopon  24924  dfii3  24928  abscncf  24946  recncf  24947  imcncf  24948  abscncfALT  24970  cnmptre  24973  iimulcnOLD  24987  icchmeo  24990  icchmeoOLD  24991  cnrehmeo  25003  cnrehmeoOLD  25004  evth  25010  evth2  25011  lebnumlem2  25013  lebnumii  25017  reparphtiOLD  25049  cphsqrtcl  25237  resscdrg  25411  ishl2  25423  recms  25433  reust  25434  evthicc  25513  evthicc2  25514  ovolfsf  25525  volcn  25660  volivth  25661  ismbf  25682  cncombf  25712  cnmbf  25713  0plef  25726  itg1ge0  25740  i1faddlem  25747  i1fmul  25750  itg1addlem4  25753  itg1addlem4OLD  25754  i1fsub  25763  itg1sub  25764  mbfi1fseqlem5  25774  xrge0f  25786  itg20  25792  itg2const  25795  itg2mulc  25802  itg2addlem  25813  i1fibl  25863  itgitg1  25864  iblabslem  25883  iblabs  25884  bddmulibl  25894  recnprss  25959  dvmptresicc  25971  dvcjbr  26007  dvfre  26009  dvnfre  26010  dvferm1  26043  dvferm2  26045  rolle  26048  cmvth  26049  cmvthOLD  26050  mvth  26051  dvlip  26052  dvlipcn  26053  dvlip2  26054  c1liplem1  26055  c1lip2  26057  dvgt0lem1  26061  dvle  26066  dvivthlem1  26067  dvivth  26069  dvne0  26070  lhop1lem  26072  lhop1  26073  lhop2  26074  lhop  26075  dvcnvrelem1  26076  dvcnvrelem2  26077  dvcnvre  26078  dvcvx  26079  dvfsumle  26080  dvfsumleOLD  26081  dvfsumge  26082  dvfsumabs  26083  dvfsumlem2  26087  dvfsumlem2OLD  26088  dvfsumrlim  26092  ftc1a  26098  ftc1lem3  26099  ftc1lem6  26102  ftc1  26103  ftc1cn  26104  ftc2  26105  ftc2ditglem  26106  itgparts  26108  itgsubstlem  26109  itgsubst  26110  itgpowd  26111  aacjcl  26387  aalioulem3  26394  taylthlem2  26434  taylthlem2OLD  26435  taylth  26436  abelth2  26504  reeff1olem  26508  efcvx  26511  pilem3  26515  pige3ALT  26580  recosf1o  26595  resinf1o  26596  dvrelog  26697  relogcn  26698  logcnlem5  26706  logcn  26707  dvloglem  26708  dvlog2lem  26712  logccv  26723  dvcxp1  26800  cxpcn3  26809  resqrtcn  26810  loglesqrt  26822  ssscongptld  26883  ressatans  26995  rlimcnp  27026  efrlim  27030  efrlimOLD  27031  jensenlem1  27048  jensenlem2  27049  jensen  27050  amgm  27052  lgamgulmlem2  27091  ftalem3  27136  basellem9  27150  efnnfsumcl  27164  efchtdvds  27220  lgsdchr  27417  dchrvmasumlem1  27557  dchrisum0lem3  27581  pntlem3  27671  cchhllem  28919  cchhllemOLD  28920  ex-fpar  30494  ipasslem7  30868  fprodex01  32829  rexdiv  32890  fsumrp0cl  33007  xrge0slmod  33341  ccfldsrarelvec  33681  ccfldextdgrr  33682  rmulccn  33874  raddcn  33875  xrge0iifhom  33883  lmlimxrge0  33894  rezh  33917  indsumin  33986  esumpfinvallem  34038  esumpfinval  34039  esumpfinvalf  34040  esumcvg  34050  plymulx0  34524  plymulx  34525  signsplypnf  34527  signsply0  34528  iblidicc  34569  rpsqrtcn  34570  ftc2re  34575  fdvposlt  34576  fdvneggt  34577  fdvposle  34578  fdvnegge  34579  itgexpif  34583  circlemeth  34617  circlemethnat  34618  circlevma  34619  circlemethhgt  34620  logdivsqrle  34627  resconn  35214  ivthALT  36301  dnicn  36458  knoppcnlem10  36468  knoppcnlem11  36469  unbdqndv2  36477  knoppndv  36500  knoppcn2  36502  broucube  37614  mblfinlem2  37618  mbfresfi  37626  ftc1cnnclem  37651  ftc1cnnc  37652  ftc1anclem3  37655  ftc1anclem5  37657  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  ftc2nc  37662  asindmre  37663  dvreasin  37666  dvreacos  37667  areacirclem1  37668  areacirclem2  37669  areacirclem3  37670  areacirclem4  37671  areacirc  37673  repwsmet  37794  rrnequiv  37795  rrntotbnd  37796  reheibor  37799  iccbnd  37800  intlewftc  42018  dvrelog2  42021  dvrelog3  42022  aks4d1p1p5  42032  resubeqsub  42405  subresre  42406  arearect  43176  areaquad  43177  k0004val0  44116  extoimad  44126  imo72b2lem0  44127  imo72b2lem2  44129  imo72b2lem1  44131  imo72b2  44134  ssrecnpr  44277  sblpnf  44279  radcnvrat  44283  lhe4.4ex1a  44298  refsumcn  44930  rr2sscn2  45281  uzsscn  45391  evthiccabs  45414  climreeq  45534  limciccioolb  45542  limcrecl  45550  limcicciooub  45558  limcleqr  45565  lptioo2cn  45566  lptioo1cn  45567  limclner  45572  liminflimsupclim  45728  resincncf  45796  cncficcgt0  45809  cncfiooicclem1  45814  cncfiooiccre  45816  jumpncnp  45819  dvcosre  45833  dvmptconst  45836  dvmptidg  45838  fperdvper  45840  dvresioo  45842  dvmulcncf  45846  dvdivcncf  45848  dvbdfbdioolem1  45849  ioodvbdlimc1lem1  45852  ioodvbdlimc1lem2  45853  ioodvbdlimc1  45854  ioodvbdlimc2lem  45855  ioodvbdlimc2  45856  itgsin0pilem1  45871  ibliccsinexp  45872  iblioosinexp  45874  itgsinexplem1  45875  itgsinexp  45876  itgcoscmulx  45890  itgsincmulx  45895  itgsubsticclem  45896  itgiccshift  45901  itgperiod  45902  itgsbtaddcnst  45903  dirkeritg  46023  dirkercncflem2  46025  dirkercncflem3  46026  dirkercncflem4  46027  dirkercncf  46028  fourierdlem16  46044  fourierdlem18  46046  fourierdlem21  46049  fourierdlem22  46050  fourierdlem39  46067  fourierdlem42  46070  fourierdlem48  46075  fourierdlem49  46076  fourierdlem53  46080  fourierdlem57  46084  fourierdlem58  46085  fourierdlem59  46086  fourierdlem60  46087  fourierdlem61  46088  fourierdlem62  46089  fourierdlem68  46095  fourierdlem70  46097  fourierdlem72  46099  fourierdlem73  46100  fourierdlem74  46101  fourierdlem75  46102  fourierdlem76  46103  fourierdlem78  46105  fourierdlem80  46107  fourierdlem83  46110  fourierdlem84  46111  fourierdlem85  46112  fourierdlem88  46115  fourierdlem89  46116  fourierdlem90  46117  fourierdlem91  46118  fourierdlem93  46120  fourierdlem94  46121  fourierdlem95  46122  fourierdlem96  46123  fourierdlem97  46124  fourierdlem98  46125  fourierdlem99  46126  fourierdlem101  46128  fourierdlem103  46130  fourierdlem104  46131  fourierdlem111  46138  fourierdlem112  46139  fourierdlem113  46140  fouriercnp  46147  sqwvfoura  46149  sqwvfourb  46150  fouriersw  46152  fouriercn  46153  etransclem2  46157  etransclem18  46173  etransclem23  46178  etransclem46  46201  rrxtopnfi  46208  rrndistlt  46211  sge0sn  46300  sge0tsms  46301  sge0f1o  46303  sge0pr  46315  sge0resplit  46327  sge0iunmptlemre  46336  sge0isummpt2  46353  hoicvr  46469  hoidmvlelem2  46517  refdivmptf  48276  refdivmptfv  48280  amgmlemALT  48897