Axiom ax-resscn 10928

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 10870	. 2 class ℝ
2		cc 10869	. 2 class ℂ
3	1, 2	wss 3887	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  10961  reex  10962  recni  10989  qsscn  12700  ioosscn  13141  unitsscn  13232  reexpcl  13799  rpexpcl  13801  reexpclz  13802  expge0  13819  expge1  13820  rlimrecl  15289  abscn2  15308  recn2  15310  imcn2  15311  climabs  15313  climre  15315  climim  15316  rlimabs  15318  rlimre  15320  rlimim  15321  caurcvgr  15385  caucvgrlem2  15386  caurcvg  15388  fsumrecl  15446  fsumrpcl  15449  fsumge0  15507  fsumre  15520  fsumim  15521  fprodrecl  15663  fprodrpcl  15666  fprodreclf  15669  fprodge0  15703  fprodge1  15705  rerisefaccl  15727  refallfaccl  15728  rprisefaccl  15733  reeff1  15829  nthruc  15961  regsumfsum  20666  rge0srg  20669  rebase  20811  re0g  20817  regsumsupp  20827  remet  23953  tgioo2  23966  xrsdsre  23973  recld2  23977  reperf  23982  iitopon  24042  dfii3  24046  abscncf  24064  recncf  24065  imcncf  24066  abscncfALT  24087  cnmptre  24090  iimulcn  24101  icchmeo  24104  cnrehmeo  24116  evth  24122  evth2  24123  lebnumlem2  24125  lebnumii  24129  reparphti  24160  cphsqrtcl  24348  resscdrg  24522  ishl2  24534  recms  24544  reust  24545  evthicc  24623  evthicc2  24624  ovolfsf  24635  volcn  24770  volivth  24771  ismbf  24792  cncombf  24822  cnmbf  24823  0plef  24836  itg1ge0  24850  i1faddlem  24857  i1fmul  24860  itg1addlem4  24863  itg1addlem4OLD  24864  i1fsub  24873  itg1sub  24874  mbfi1fseqlem5  24884  xrge0f  24896  itg20  24902  itg2const  24905  itg2mulc  24912  itg2addlem  24923  i1fibl  24972  itgitg1  24973  iblabslem  24992  iblabs  24993  bddmulibl  25003  recnprss  25068  dvmptresicc  25080  dvcjbr  25113  dvfre  25115  dvnfre  25116  dvferm1  25149  dvferm2  25151  rolle  25154  cmvth  25155  mvth  25156  dvlip  25157  dvlipcn  25158  dvlip2  25159  c1liplem1  25160  c1lip2  25162  dvgt0lem1  25166  dvle  25171  dvivthlem1  25172  dvivth  25174  dvne0  25175  lhop1lem  25177  lhop1  25178  lhop2  25179  lhop  25180  dvcnvrelem1  25181  dvcnvrelem2  25182  dvcnvre  25183  dvcvx  25184  dvfsumle  25185  dvfsumge  25186  dvfsumabs  25187  dvfsumlem2  25191  dvfsumrlim  25195  ftc1a  25201  ftc1lem3  25202  ftc1lem6  25205  ftc1  25206  ftc1cn  25207  ftc2  25208  ftc2ditglem  25209  itgparts  25211  itgsubstlem  25212  itgsubst  25213  itgpowd  25214  aacjcl  25487  aalioulem3  25494  taylthlem2  25533  taylth  25534  abelth2  25601  reeff1olem  25605  efcvx  25608  pilem3  25612  pige3ALT  25676  recosf1o  25691  resinf1o  25692  dvrelog  25792  relogcn  25793  logcnlem5  25801  logcn  25802  dvloglem  25803  dvlog2lem  25807  logccv  25818  dvcxp1  25893  cxpcn3  25901  resqrtcn  25902  loglesqrt  25911  ssscongptld  25972  ressatans  26084  rlimcnp  26115  efrlim  26119  jensenlem1  26136  jensenlem2  26137  jensen  26138  amgm  26140  lgamgulmlem2  26179  ftalem3  26224  basellem9  26238  efnnfsumcl  26252  efchtdvds  26308  lgsdchr  26503  dchrvmasumlem1  26643  dchrisum0lem3  26667  pntlem3  26757  cchhllem  27254  cchhllemOLD  27255  ex-fpar  28826  ipasslem7  29198  fprodex01  31139  rexdiv  31200  fsumrp0cl  31304  xrge0slmod  31548  ccfldsrarelvec  31741  ccfldextdgrr  31742  rmulccn  31878  raddcn  31879  xrge0iifhom  31887  lmlimxrge0  31898  rezh  31921  indsumin  31990  esumpfinvallem  32042  esumpfinval  32043  esumpfinvalf  32044  esumcvg  32054  plymulx0  32526  plymulx  32527  signsplypnf  32529  signsply0  32530  iblidicc  32572  rpsqrtcn  32573  ftc2re  32578  fdvposlt  32579  fdvneggt  32580  fdvposle  32581  fdvnegge  32582  itgexpif  32586  circlemeth  32620  circlemethnat  32621  circlevma  32622  circlemethhgt  32623  logdivsqrle  32630  cvxpconn  33204  cvxsconn  33205  resconn  33208  ivthALT  34524  dnicn  34672  knoppcnlem10  34682  knoppcnlem11  34683  unbdqndv2  34691  knoppndv  34714  knoppcn2  34716  broucube  35811  mblfinlem2  35815  mbfresfi  35823  ftc1cnnclem  35848  ftc1cnnc  35849  ftc1anclem3  35852  ftc1anclem5  35854  ftc1anclem7  35856  ftc1anclem8  35857  ftc1anc  35858  ftc2nc  35859  asindmre  35860  dvreasin  35863  dvreacos  35864  areacirclem1  35865  areacirclem2  35866  areacirclem3  35867  areacirclem4  35868  areacirc  35870  repwsmet  35992  rrnequiv  35993  rrntotbnd  35994  reheibor  35997  iccbnd  35998  intlewftc  40069  dvrelog2  40072  dvrelog3  40073  aks4d1p1p5  40083  resubeqsub  40411  subresre  40412  arearect  41046  areaquad  41047  k0004val0  41764  extoimad  41775  imo72b2lem0  41776  imo72b2lem2  41778  imo72b2lem1  41780  imo72b2  41783  ssrecnpr  41926  sblpnf  41928  radcnvrat  41932  lhe4.4ex1a  41947  refsumcn  42573  rr2sscn2  42905  uzsscn  43016  evthiccabs  43034  climreeq  43154  limciccioolb  43162  limcrecl  43170  limcicciooub  43178  limcleqr  43185  lptioo2cn  43186  lptioo1cn  43187  limclner  43192  liminflimsupclim  43348  resincncf  43416  cncficcgt0  43429  cncfiooicclem1  43434  cncfiooiccre  43436  jumpncnp  43439  dvcosre  43453  dvmptconst  43456  dvmptidg  43458  fperdvper  43460  dvresioo  43462  dvmulcncf  43466  dvdivcncf  43468  dvbdfbdioolem1  43469  ioodvbdlimc1lem1  43472  ioodvbdlimc1lem2  43473  ioodvbdlimc1  43474  ioodvbdlimc2lem  43475  ioodvbdlimc2  43476  itgsin0pilem1  43491  ibliccsinexp  43492  iblioosinexp  43494  itgsinexplem1  43495  itgsinexp  43496  itgcoscmulx  43510  itgsincmulx  43515  itgsubsticclem  43516  itgiccshift  43521  itgperiod  43522  itgsbtaddcnst  43523  dirkeritg  43643  dirkercncflem2  43645  dirkercncflem3  43646  dirkercncflem4  43647  dirkercncf  43648  fourierdlem16  43664  fourierdlem18  43666  fourierdlem21  43669  fourierdlem22  43670  fourierdlem39  43687  fourierdlem42  43690  fourierdlem48  43695  fourierdlem49  43696  fourierdlem53  43700  fourierdlem57  43704  fourierdlem58  43705  fourierdlem59  43706  fourierdlem60  43707  fourierdlem61  43708  fourierdlem62  43709  fourierdlem68  43715  fourierdlem70  43717  fourierdlem72  43719  fourierdlem73  43720  fourierdlem74  43721  fourierdlem75  43722  fourierdlem76  43723  fourierdlem78  43725  fourierdlem80  43727  fourierdlem83  43730  fourierdlem84  43731  fourierdlem85  43732  fourierdlem88  43735  fourierdlem89  43736  fourierdlem90  43737  fourierdlem91  43738  fourierdlem93  43740  fourierdlem94  43741  fourierdlem95  43742  fourierdlem96  43743  fourierdlem97  43744  fourierdlem98  43745  fourierdlem99  43746  fourierdlem101  43748  fourierdlem103  43750  fourierdlem104  43751  fourierdlem111  43758  fourierdlem112  43759  fourierdlem113  43760  fouriercnp  43767  sqwvfoura  43769  sqwvfourb  43770  fouriersw  43772  fouriercn  43773  etransclem2  43777  etransclem18  43793  etransclem23  43798  etransclem46  43821  rrxtopnfi  43828  rrndistlt  43831  sge0sn  43917  sge0tsms  43918  sge0f1o  43920  sge0pr  43932  sge0resplit  43944  sge0iunmptlemre  43953  sge0isummpt2  43970  hoicvr  44086  hoidmvlelem2  44134  refdivmptf  45888  refdivmptfv  45892  amgmlemALT  46507