Axiom ax-resscn 10331

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 10273	. 2 class ℝ
2		cc 10272	. 2 class ℂ
3	1, 2	wss 3792	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  10364  reex  10365  recni  10393  nnsscnOLD  11385  nn0sscnOLD  11653  qsscn  12112  reexpcl  13200  rpexpcl  13202  reexpclz  13203  expge0  13219  expge1  13220  rlimrecl  14728  abscn2  14746  recn2  14748  imcn2  14749  climabs  14751  climre  14753  climim  14754  rlimabs  14756  rlimre  14758  rlimim  14759  caurcvgr  14821  caucvgrlem2  14822  caurcvg  14824  fsumrecl  14881  fsumrpcl  14884  fsumge0  14940  fsumre  14953  fsumim  14954  fprodrecl  15095  fprodrpcl  15098  fprodreclf  15101  fprodge0  15135  fprodge1  15137  rerisefaccl  15159  refallfaccl  15160  rprisefaccl  15165  reeff1  15261  nthruc  15394  regsumfsum  20221  rge0srg  20224  rebase  20360  re0g  20366  regsumsupp  20376  remet  23012  tgioo2  23025  xrsdsre  23032  recld2  23036  reperf  23041  iitopon  23101  dfii3  23105  abscncf  23123  recncf  23124  imcncf  23125  abscncfALT  23142  cnmptre  23145  iimulcn  23156  icchmeo  23159  cnrehmeo  23171  evth  23177  evth2  23178  lebnumlem2  23180  lebnumii  23184  reparphti  23215  cphsqrtcl  23402  resscdrg  23575  ishl2  23587  recms  23597  reust  23598  evthicc  23674  evthicc2  23675  ovolfsf  23686  volcn  23821  volivth  23822  ismbf  23843  cncombf  23873  cnmbf  23874  0plef  23887  itg1ge0  23901  i1faddlem  23908  i1fmul  23911  itg1addlem4  23914  i1fsub  23923  itg1sub  23924  mbfi1fseqlem5  23934  xrge0f  23946  itg20  23952  itg2const  23955  itg2mulc  23962  itg2addlem  23973  i1fibl  24022  itgitg1  24023  iblabslem  24042  iblabs  24043  bddmulibl  24053  recnprss  24116  dvcjbr  24160  dvfre  24162  dvnfre  24163  dvferm1  24196  dvferm2  24198  rolle  24201  cmvth  24202  mvth  24203  dvlip  24204  dvlipcn  24205  dvlip2  24206  c1liplem1  24207  c1lip2  24209  dvgt0lem1  24213  dvle  24218  dvivthlem1  24219  dvivth  24221  dvne0  24222  lhop1lem  24224  lhop1  24225  lhop2  24226  lhop  24227  dvcnvrelem1  24228  dvcnvrelem2  24229  dvcnvre  24230  dvcvx  24231  dvfsumle  24232  dvfsumge  24233  dvfsumabs  24234  dvfsumlem2  24238  dvfsumrlim  24242  ftc1a  24248  ftc1lem3  24249  ftc1lem6  24252  ftc1  24253  ftc1cn  24254  ftc2  24255  ftc2ditglem  24256  itgparts  24258  itgsubstlem  24259  itgsubst  24260  aacjcl  24530  aalioulem3  24537  taylthlem2  24576  taylth  24577  abelth2  24644  reeff1olem  24648  efcvx  24651  pilem3  24655  pilem3OLD  24656  pige3  24718  recosf1o  24730  resinf1o  24731  dvrelog  24831  relogcn  24832  logcnlem5  24840  logcn  24841  dvloglem  24842  dvlog2lem  24846  logccv  24857  dvcxp1  24932  cxpcn3  24940  resqrtcn  24941  loglesqrt  24950  ssscongptld  25011  ressatans  25123  rlimcnp  25155  efrlim  25159  jensenlem1  25176  jensenlem2  25177  jensen  25178  amgm  25180  lgamgulmlem2  25219  ftalem3  25264  basellem9  25278  efnnfsumcl  25292  efchtdvds  25348  lgsdchr  25543  dchrvmasumlem1  25653  dchrisum0lem3  25677  pntlem3  25767  cchhllem  26253  ipasslem7  28280  fprodex01  30149  rexdiv  30210  fsumrp0cl  30265  xrge0slmod  30414  unitsscn  30548  rmulccn  30580  raddcn  30581  xrge0iifhom  30589  lmlimxrge0  30600  rezh  30621  indsumin  30690  esumpfinvallem  30742  esumpfinval  30743  esumpfinvalf  30744  esumcvg  30754  plymulx0  31232  plymulx  31233  signsplypnf  31235  signsply0  31236  iblidicc  31280  rpsqrtcn  31281  ftc2re  31286  fdvposlt  31287  fdvneggt  31288  fdvposle  31289  fdvnegge  31290  itgexpif  31294  circlemeth  31328  circlemethnat  31329  circlevma  31330  circlemethhgt  31331  logdivsqrle  31338  cvxpconn  31831  cvxsconn  31832  resconn  31835  ivthALT  32926  dnicn  33073  knoppcnlem10  33083  knoppcnlem11  33084  unbdqndv2  33092  knoppndv  33115  knoppcn2  33117  broucube  34078  mblfinlem2  34082  mbfresfi  34090  ftc1cnnclem  34117  ftc1cnnc  34118  ftc1anclem3  34121  ftc1anclem5  34123  ftc1anclem7  34125  ftc1anclem8  34126  ftc1anc  34127  ftc2nc  34128  asindmre  34129  dvreasin  34132  dvreacos  34133  areacirclem1  34134  areacirclem2  34135  areacirclem3  34136  areacirclem4  34137  areacirc  34139  repwsmet  34266  rrnequiv  34267  rrntotbnd  34268  reheibor  34271  iccbnd  34272  itgpowd  38772  arearect  38773  areaquad  38774  k0004val0  39422  extoimad  39434  imo72b2lem0  39435  imo72b2lem2  39437  imo72b2lem1  39441  imo72b2  39445  ssrecnpr  39477  sblpnf  39479  radcnvrat  39483  lhe4.4ex1a  39498  refsumcn  40136  rr2sscn2  40504  uzsscn  40625  ioosscn  40642  evthiccabs  40644  climreeq  40767  limciccioolb  40775  limcrecl  40783  limcicciooub  40791  limcleqr  40798  lptioo2cn  40799  lptioo1cn  40800  limclner  40805  liminflimsupclim  40961  resincncf  41030  cncficcgt0  41043  cncfiooicclem1  41048  cncfiooiccre  41050  jumpncnp  41053  dvcosre  41068  dvmptconst  41071  dvmptidg  41073  fperdvper  41075  dvmptresicc  41076  dvresioo  41078  dvmulcncf  41082  dvdivcncf  41084  dvbdfbdioolem1  41085  ioodvbdlimc1lem1  41088  ioodvbdlimc1lem2  41089  ioodvbdlimc1  41090  ioodvbdlimc2lem  41091  ioodvbdlimc2  41092  itgsin0pilem1  41107  ibliccsinexp  41108  iblioosinexp  41110  itgsinexplem1  41111  itgsinexp  41112  itgcoscmulx  41126  itgsincmulx  41131  itgsubsticclem  41132  itgiccshift  41137  itgperiod  41138  itgsbtaddcnst  41139  dirkeritg  41260  dirkercncflem2  41262  dirkercncflem3  41263  dirkercncflem4  41264  dirkercncf  41265  fourierdlem16  41281  fourierdlem18  41283  fourierdlem21  41286  fourierdlem22  41287  fourierdlem39  41304  fourierdlem42  41307  fourierdlem48  41312  fourierdlem49  41313  fourierdlem53  41317  fourierdlem57  41321  fourierdlem58  41322  fourierdlem59  41323  fourierdlem60  41324  fourierdlem61  41325  fourierdlem62  41326  fourierdlem68  41332  fourierdlem70  41334  fourierdlem72  41336  fourierdlem73  41337  fourierdlem74  41338  fourierdlem75  41339  fourierdlem76  41340  fourierdlem78  41342  fourierdlem80  41344  fourierdlem83  41347  fourierdlem84  41348  fourierdlem85  41349  fourierdlem88  41352  fourierdlem89  41353  fourierdlem90  41354  fourierdlem91  41355  fourierdlem93  41357  fourierdlem94  41358  fourierdlem95  41359  fourierdlem96  41360  fourierdlem97  41361  fourierdlem98  41362  fourierdlem99  41363  fourierdlem101  41365  fourierdlem103  41367  fourierdlem104  41368  fourierdlem111  41375  fourierdlem112  41376  fourierdlem113  41377  fouriercnp  41384  sqwvfoura  41386  sqwvfourb  41387  fouriersw  41389  fouriercn  41390  etransclem2  41394  etransclem18  41410  etransclem23  41415  etransclem46  41438  rrxtopnfi  41445  rrndistlt  41448  sge0sn  41534  sge0tsms  41535  sge0f1o  41537  sge0pr  41549  sge0resplit  41561  sge0iunmptlemre  41570  sge0isummpt2  41587  hoicvr  41703  hoidmvlelem2  41751  refdivmptf  43365  refdivmptfv  43369  amgmlemALT  43669