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

Axiom ax-resscn 8881
Description: The real numbers are a subset of the complex numbers. Axiom 1 of 22 for real and complex numbers, justified by theorem axresscn 8857. (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 8823 . 2  class  RR
2 cc 8822 . 2  class  CC
31, 2wss 3228 1  wff  RR  C_  CC
Colors of variables: wff set class
This axiom is referenced by:  recn  8914  reex  8915  recni  8936  nnsscn  9838  nn0sscn  10059  qsscn  10416  reexpcl  11210  rpexpcl  11212  reexpclz  11213  expge0  11228  expge1  11229  rlimrecl  12144  abscn2  12162  recn2  12164  imcn2  12165  climabs  12167  climre  12169  climim  12170  rlimabs  12172  rlimre  12174  rlimim  12175  caurcvgr  12237  caucvgrlem2  12238  caurcvg  12240  fsumrecl  12298  fsumrpcl  12301  fsumge0  12344  fsumre  12357  fsumim  12358  reeff1  12491  nthruc  12620  remet  18392  tgioo2  18405  xrsdsre  18412  recld2  18416  reperf  18421  iitopon  18480  dfii3  18484  abscncf  18502  recncf  18503  imcncf  18504  abscncfALT  18521  cnmptre  18523  iimulcn  18534  icchmeo  18537  cnrehmeo  18549  evth  18555  evth2  18556  lebnumlem2  18558  lebnumii  18562  reparphti  18593  cphsqrcl  18718  resscdrg  18873  ishl2  18885  evthicc  18917  evthicc2  18918  ovolfsf  18929  volcn  19059  volivth  19060  ismbf  19083  cncombf  19111  cnmbf  19112  0plef  19125  itg1ge0  19139  i1faddlem  19146  i1fmul  19149  itg1addlem4  19152  i1fsub  19161  itg1sub  19162  mbfi1fseqlem5  19172  xrge0f  19184  itg20  19190  itg2const  19193  itg2mulc  19200  itg2addlem  19211  i1fibl  19260  itgitg1  19261  iblabslem  19280  iblabs  19281  bddmulibl  19291  recnprss  19352  dvcjbr  19396  dvfre  19398  dvnfre  19399  dvferm1  19430  dvferm2  19432  rolle  19435  cmvth  19436  mvth  19437  dvlip  19438  dvlipcn  19439  dvlip2  19440  c1liplem1  19441  c1lip2  19443  dvgt0lem1  19447  dvle  19452  dvivthlem1  19453  dvivth  19455  dvne0  19456  lhop1lem  19458  lhop1  19459  lhop2  19460  lhop  19461  dvcnvrelem1  19462  dvcnvrelem2  19463  dvcnvre  19464  dvcvx  19465  dvfsumle  19466  dvfsumge  19467  dvfsumabs  19468  dvfsumlem2  19472  dvfsumrlim  19476  ftc1a  19482  ftc1lem3  19483  ftc1lem6  19486  ftc1  19487  ftc1cn  19488  ftc2  19489  ftc2ditglem  19490  itgparts  19492  itgsubstlem  19493  itgsubst  19494  aacjcl  19805  aalioulem3  19812  taylthlem2  19851  taylth  19852  abelth2  19919  reeff1olem  19923  efcvx  19926  pilem3  19930  pige3  19986  recosf1o  19998  resinf1o  19999  dvrelog  20089  relogcn  20090  logcnlem5  20098  logcn  20099  dvloglem  20100  dvlog2lem  20104  logccv  20115  dvcxp1  20187  cxpcn3  20193  resqrcn  20194  loglesqr  20203  ssscongptld  20227  ressatans  20335  rlimcnp  20365  efrlim  20369  jensenlem1  20386  jensenlem2  20387  jensen  20388  amgm  20390  ftalem3  20418  basellem9  20432  efnnfsumcl  20446  efchtdvds  20503  lgsdchr  20693  dchrvmasumlem1  20750  dchrisum0lem3  20774  pntlem3  20864  readdsubgo  21126  circgrp  21147  ipasslem7  21522  rexdiv  23376  fsumrp0cl  23409  rebase  23435  re0g  23438  unitsscn  23450  rmulccn  23470  raddcn  23471  xrge0iifhom  23479  lmlimxrge0  23490  recms  23619  recusp  23620  esumpfinvallem  23730  esumpfinval  23731  esumpfinvalf  23732  esumcvg  23742  dya2icoseg2  23892  lgamgulmlem2  24063  cvxpcon  24177  cvxscon  24178  rescon  24181  fprodrecl  24580  fprodrpcl  24583  rerisefaccl  24623  refallfaccl  24624  rprisefaccl  24629  ftc1cnnclem  25513  ftc1cnnc  25514  dvreasin  25515  dvreacos  25516  areacirclem2  25517  areacirclem3  25518  areacirclem4  25519  areacirclem1  25520  areacirclem5  25521  areacirc  25523  ivthALT  25582  repwsmet  25881  rrnequiv  25882  rrntotbnd  25883  reheibor  25886  iccbnd  25887  ssrecnpr  26860  sblpnf  26862  lhe4.4ex1a  26869  refsumcn  27024  climreeq  27062  dvcosre  27064  ibliccsinexp  27068  iblioosinexp  27070  itgsinexplem1  27071  itgsinexp  27072  wallispilem2  27138  wallispilem4  27140  wallispi  27142
  Copyright terms: Public domain W3C validator