Axiom ax-resscn 11209

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 11151	. 2 class ℝ
2		cc 11150	. 2 class ℂ
3	1, 2	wss 3962	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  11242  reex  11243  recni  11272  qsscn  12999  ioosscn  13445  unitsscn  13536  reexpcl  14115  rpexpcl  14117  reexpclz  14119  expge0  14135  expge1  14136  rlimrecl  15612  abscn2  15631  recn2  15633  imcn2  15634  climabs  15636  climre  15638  climim  15639  rlimabs  15641  rlimre  15643  rlimim  15644  caurcvgr  15706  caucvgrlem2  15707  caurcvg  15709  fsumrecl  15766  fsumrpcl  15769  fsumge0  15827  fsumre  15840  fsumim  15841  fprodrecl  15985  fprodrpcl  15988  fprodreclf  15991  fprodge0  16025  fprodge1  16027  rerisefaccl  16049  refallfaccl  16050  rprisefaccl  16055  reeff1  16152  nthruc  16284  regsumfsum  21470  rge0srg  21473  rebase  21641  re0g  21647  regsumsupp  21657  remet  24825  tgioo2  24838  xrsdsre  24845  recld2  24849  reperf  24854  iitopon  24918  dfii3  24922  abscncf  24940  recncf  24941  imcncf  24942  abscncfALT  24964  cnmptre  24967  iimulcnOLD  24981  icchmeo  24984  icchmeoOLD  24985  cnrehmeo  24997  cnrehmeoOLD  24998  evth  25004  evth2  25005  lebnumlem2  25007  lebnumii  25011  reparphtiOLD  25043  cphsqrtcl  25231  resscdrg  25405  ishl2  25417  recms  25427  reust  25428  evthicc  25507  evthicc2  25508  ovolfsf  25519  volcn  25654  volivth  25655  ismbf  25676  cncombf  25706  cnmbf  25707  0plef  25720  itg1ge0  25734  i1faddlem  25741  i1fmul  25744  itg1addlem4  25747  itg1addlem4OLD  25748  i1fsub  25757  itg1sub  25758  mbfi1fseqlem5  25768  xrge0f  25780  itg20  25786  itg2const  25789  itg2mulc  25796  itg2addlem  25807  i1fibl  25857  itgitg1  25858  iblabslem  25877  iblabs  25878  bddmulibl  25888  recnprss  25953  dvmptresicc  25965  dvcjbr  26001  dvfre  26003  dvnfre  26004  dvferm1  26037  dvferm2  26039  rolle  26042  cmvth  26043  cmvthOLD  26044  mvth  26045  dvlip  26046  dvlipcn  26047  dvlip2  26048  c1liplem1  26049  c1lip2  26051  dvgt0lem1  26055  dvle  26060  dvivthlem1  26061  dvivth  26063  dvne0  26064  lhop1lem  26066  lhop1  26067  lhop2  26068  lhop  26069  dvcnvrelem1  26070  dvcnvrelem2  26071  dvcnvre  26072  dvcvx  26073  dvfsumle  26074  dvfsumleOLD  26075  dvfsumge  26076  dvfsumabs  26077  dvfsumlem2  26081  dvfsumlem2OLD  26082  dvfsumrlim  26086  ftc1a  26092  ftc1lem3  26093  ftc1lem6  26096  ftc1  26097  ftc1cn  26098  ftc2  26099  ftc2ditglem  26100  itgparts  26102  itgsubstlem  26103  itgsubst  26104  itgpowd  26105  aacjcl  26383  aalioulem3  26390  taylthlem2  26430  taylthlem2OLD  26431  taylth  26432  abelth2  26500  reeff1olem  26504  efcvx  26507  pilem3  26511  pige3ALT  26576  recosf1o  26591  resinf1o  26592  dvrelog  26693  relogcn  26694  logcnlem5  26702  logcn  26703  dvloglem  26704  dvlog2lem  26708  logccv  26719  dvcxp1  26796  cxpcn3  26805  resqrtcn  26806  loglesqrt  26818  ssscongptld  26879  ressatans  26991  rlimcnp  27022  efrlim  27026  efrlimOLD  27027  jensenlem1  27044  jensenlem2  27045  jensen  27046  amgm  27048  lgamgulmlem2  27087  ftalem3  27132  basellem9  27146  efnnfsumcl  27160  efchtdvds  27216  lgsdchr  27413  dchrvmasumlem1  27553  dchrisum0lem3  27577  pntlem3  27667  cchhllem  28915  cchhllemOLD  28916  ex-fpar  30490  ipasslem7  30864  fprodex01  32831  rexdiv  32892  fsumrp0cl  33008  xrge0slmod  33355  ccfldsrarelvec  33695  ccfldextdgrr  33696  rmulccn  33888  raddcn  33889  xrge0iifhom  33897  lmlimxrge0  33908  rezh  33931  indsumin  34002  esumpfinvallem  34054  esumpfinval  34055  esumpfinvalf  34056  esumcvg  34066  plymulx0  34540  plymulx  34541  signsplypnf  34543  signsply0  34544  iblidicc  34585  rpsqrtcn  34586  ftc2re  34591  fdvposlt  34592  fdvneggt  34593  fdvposle  34594  fdvnegge  34595  itgexpif  34599  circlemeth  34633  circlemethnat  34634  circlevma  34635  circlemethhgt  34636  logdivsqrle  34643  resconn  35230  ivthALT  36317  dnicn  36474  knoppcnlem10  36484  knoppcnlem11  36485  unbdqndv2  36493  knoppndv  36516  knoppcn2  36518  broucube  37640  mblfinlem2  37644  mbfresfi  37652  ftc1cnnclem  37677  ftc1cnnc  37678  ftc1anclem3  37681  ftc1anclem5  37683  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  ftc2nc  37688  asindmre  37689  dvreasin  37692  dvreacos  37693  areacirclem1  37694  areacirclem2  37695  areacirclem3  37696  areacirclem4  37697  areacirc  37699  repwsmet  37820  rrnequiv  37821  rrntotbnd  37822  reheibor  37825  iccbnd  37826  intlewftc  42042  dvrelog2  42045  dvrelog3  42046  aks4d1p1p5  42056  rpsscn  42311  redvmptabs  42368  readvrec2  42369  resubeqsub  42435  subresre  42436  arearect  43203  areaquad  43204  k0004val0  44143  extoimad  44153  imo72b2lem0  44154  imo72b2lem2  44156  imo72b2lem1  44158  imo72b2  44161  ssrecnpr  44303  sblpnf  44305  radcnvrat  44309  lhe4.4ex1a  44324  refsumcn  44967  rr2sscn2  45315  uzsscn  45425  evthiccabs  45448  climreeq  45568  limciccioolb  45576  limcrecl  45584  limcicciooub  45592  limcleqr  45599  lptioo2cn  45600  lptioo1cn  45601  limclner  45606  liminflimsupclim  45762  resincncf  45830  cncficcgt0  45843  cncfiooicclem1  45848  cncfiooiccre  45850  jumpncnp  45853  dvcosre  45867  dvmptconst  45870  dvmptidg  45872  fperdvper  45874  dvresioo  45876  dvmulcncf  45880  dvdivcncf  45882  dvbdfbdioolem1  45883  ioodvbdlimc1lem1  45886  ioodvbdlimc1lem2  45887  ioodvbdlimc1  45888  ioodvbdlimc2lem  45889  ioodvbdlimc2  45890  itgsin0pilem1  45905  ibliccsinexp  45906  iblioosinexp  45908  itgsinexplem1  45909  itgsinexp  45910  itgcoscmulx  45924  itgsincmulx  45929  itgsubsticclem  45930  itgiccshift  45935  itgperiod  45936  itgsbtaddcnst  45937  dirkeritg  46057  dirkercncflem2  46059  dirkercncflem3  46060  dirkercncflem4  46061  dirkercncf  46062  fourierdlem16  46078  fourierdlem18  46080  fourierdlem21  46083  fourierdlem22  46084  fourierdlem39  46101  fourierdlem42  46104  fourierdlem48  46109  fourierdlem49  46110  fourierdlem53  46114  fourierdlem57  46118  fourierdlem58  46119  fourierdlem59  46120  fourierdlem60  46121  fourierdlem61  46122  fourierdlem62  46123  fourierdlem68  46129  fourierdlem70  46131  fourierdlem72  46133  fourierdlem73  46134  fourierdlem74  46135  fourierdlem75  46136  fourierdlem76  46137  fourierdlem78  46139  fourierdlem80  46141  fourierdlem83  46144  fourierdlem84  46145  fourierdlem85  46146  fourierdlem88  46149  fourierdlem89  46150  fourierdlem90  46151  fourierdlem91  46152  fourierdlem93  46154  fourierdlem94  46155  fourierdlem95  46156  fourierdlem96  46157  fourierdlem97  46158  fourierdlem98  46159  fourierdlem99  46160  fourierdlem101  46162  fourierdlem103  46164  fourierdlem104  46165  fourierdlem111  46172  fourierdlem112  46173  fourierdlem113  46174  fouriercnp  46181  sqwvfoura  46183  sqwvfourb  46184  fouriersw  46186  fouriercn  46187  etransclem2  46191  etransclem18  46207  etransclem23  46212  etransclem46  46235  rrxtopnfi  46242  rrndistlt  46245  sge0sn  46334  sge0tsms  46335  sge0f1o  46337  sge0pr  46349  sge0resplit  46361  sge0iunmptlemre  46370  sge0isummpt2  46387  hoicvr  46503  hoidmvlelem2  46551  refdivmptf  48391  refdivmptfv  48395  amgmlemALT  49033