MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-resscn Unicode version

Axiom ax-resscn 8794
Description: The real numbers are a subset of the complex numbers. Axiom 1 of 22 for real and complex numbers, justified by theorem axresscn 8770. (Contributed by NM, 1-Mar-1995.)
Assertion
Ref Expression
ax-resscn  |-  RR  C_  CC

Detailed syntax breakdown of Axiom ax-resscn
StepHypRef Expression
1 cr 8736 . 2  class  RR
2 cc 8735 . 2  class  CC
31, 2wss 3152 1  wff  RR  C_  CC
Colors of variables: wff set class
This axiom is referenced by:  recn  8827  reex  8828  recni  8849  nnsscn  9751  nn0sscn  9970  qsscn  10327  reexpcl  11120  rpexpcl  11122  reexpclz  11123  expge0  11138  expge1  11139  rlimrecl  12054  abscn2  12072  recn2  12074  imcn2  12075  climabs  12077  climre  12079  climim  12080  rlimabs  12082  rlimre  12084  rlimim  12085  caurcvgr  12146  caucvgrlem2  12147  caurcvg  12149  fsumrecl  12207  fsumrpcl  12210  fsumge0  12253  fsumre  12266  fsumim  12267  reeff1  12400  nthruc  12529  remet  18296  tgioo2  18309  xrsdsre  18316  recld2  18320  reperf  18324  iitopon  18383  dfii3  18387  abscncf  18405  recncf  18406  imcncf  18407  abscncfALT  18423  cnmptre  18425  iimulcn  18436  icchmeo  18439  cnrehmeo  18451  evth  18457  evth2  18458  lebnumlem2  18460  lebnumii  18464  reparphti  18495  cphsqrcl  18620  resscdrg  18775  ishl2  18787  evthicc  18819  evthicc2  18820  ovolfsf  18831  volcn  18961  volivth  18962  ismbf  18985  cncombf  19013  cnmbf  19014  0plef  19027  itg1ge0  19041  i1faddlem  19048  i1fmul  19051  itg1addlem4  19054  i1fsub  19063  itg1sub  19064  mbfi1fseqlem5  19074  xrge0f  19086  itg20  19092  itg2const  19095  itg2mulc  19102  itg2addlem  19113  i1fibl  19162  itgitg1  19163  iblabslem  19182  iblabs  19183  bddmulibl  19193  recnprss  19254  dvcjbr  19298  dvfre  19300  dvnfre  19301  dvferm1  19332  dvferm2  19334  rolle  19337  cmvth  19338  mvth  19339  dvlip  19340  dvlipcn  19341  dvlip2  19342  c1liplem1  19343  c1lip2  19345  dvgt0lem1  19349  dvle  19354  dvivthlem1  19355  dvivth  19357  dvne0  19358  lhop1lem  19360  lhop1  19361  lhop2  19362  lhop  19363  dvcnvrelem1  19364  dvcnvrelem2  19365  dvcnvre  19366  dvcvx  19367  dvfsumle  19368  dvfsumge  19369  dvfsumabs  19370  dvfsumlem2  19374  dvfsumrlim  19378  ftc1a  19384  ftc1lem3  19385  ftc1lem6  19388  ftc1  19389  ftc1cn  19390  ftc2  19391  ftc2ditglem  19392  itgparts  19394  itgsubstlem  19395  itgsubst  19396  aacjcl  19707  aalioulem3  19714  taylthlem2  19753  taylth  19754  abelth2  19818  reeff1olem  19822  efcvx  19825  pilem3  19829  pige3  19885  recosf1o  19897  resinf1o  19898  dvrelog  19984  relogcn  19985  logcnlem5  19993  logcn  19994  dvloglem  19995  dvlog2lem  19999  logccv  20010  dvcxp1  20082  cxpcn3  20088  resqrcn  20089  loglesqr  20098  ssscongptld  20122  ressatans  20230  rlimcnp  20260  efrlim  20264  jensenlem1  20281  jensenlem2  20282  jensen  20283  amgm  20285  ftalem3  20312  basellem9  20326  efnnfsumcl  20340  efchtdvds  20397  lgsdchr  20587  dchrvmasumlem1  20644  dchrisum0lem3  20668  pntlem3  20758  readdsubgo  21020  circgrp  21041  ipasslem7  21414  rexdiv  23109  unitsscn  23280  rmulccn  23301  raddcn  23302  xrge0iifhom  23319  fsumrp0cl  23334  lmlimxrge0  23372  esumpfinvallem  23442  esumpfinval  23443  esumpfinvalf  23444  esumcvg  23454  cvxpcon  23773  cvxscon  23774  rescon  23777  dvreasin  24923  dvreacos  24924  areacirclem2  24925  areacirclem3  24926  areacirclem4  24927  areacirclem1  24928  areacirclem5  24929  areacirc  24931  claddrvr  25648  rnegvex2  25661  negveudr  25669  subclrvd  25674  clsmulrv  25683  divclrvd  25695  ivthALT  26258  repwsmet  26558  rrnequiv  26559  rrntotbnd  26560  reheibor  26563  iccbnd  26564  ssrecnpr  27537  sblpnf  27539  lhe4.4ex1a  27546  refsumcn  27701  climreeq  27739  dvcosre  27741  ibliccsinexp  27745  iblioosinexp  27747  itgsinexplem1  27748  itgsinexp  27749  wallispilem2  27815  wallispilem4  27817  wallispi  27819
  Copyright terms: Public domain W3C validator