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

Axiom ax-resscn 9047
Description: The real numbers are a subset of the complex numbers. Axiom 1 of 22 for real and complex numbers, justified by theorem axresscn 9023. (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 8989 . 2  class  RR
2 cc 8988 . 2  class  CC
31, 2wss 3320 1  wff  RR  C_  CC
Colors of variables: wff set class
This axiom is referenced by:  recn  9080  reex  9081  recni  9102  nnsscn  10005  nn0sscn  10226  qsscn  10585  reexpcl  11398  rpexpcl  11400  reexpclz  11401  expge0  11416  expge1  11417  rlimrecl  12374  abscn2  12392  recn2  12394  imcn2  12395  climabs  12397  climre  12399  climim  12400  rlimabs  12402  rlimre  12404  rlimim  12405  caurcvgr  12467  caucvgrlem2  12468  caurcvg  12470  fsumrecl  12528  fsumrpcl  12531  fsumge0  12574  fsumre  12587  fsumim  12588  reeff1  12721  nthruc  12850  remet  18821  tgioo2  18834  xrsdsre  18841  recld2  18845  reperf  18850  iitopon  18909  dfii3  18913  abscncf  18931  recncf  18932  imcncf  18933  abscncfALT  18950  cnmptre  18952  iimulcn  18963  icchmeo  18966  cnrehmeo  18978  evth  18984  evth2  18985  lebnumlem2  18987  lebnumii  18991  reparphti  19022  cphsqrcl  19147  resscdrg  19312  ishl2  19324  evthicc  19356  evthicc2  19357  ovolfsf  19368  volcn  19498  volivth  19499  ismbf  19522  cncombf  19550  cnmbf  19551  0plef  19564  itg1ge0  19578  i1faddlem  19585  i1fmul  19588  itg1addlem4  19591  i1fsub  19600  itg1sub  19601  mbfi1fseqlem5  19611  xrge0f  19623  itg20  19629  itg2const  19632  itg2mulc  19639  itg2addlem  19650  i1fibl  19699  itgitg1  19700  iblabslem  19719  iblabs  19720  bddmulibl  19730  recnprss  19791  dvcjbr  19835  dvfre  19837  dvnfre  19838  dvferm1  19869  dvferm2  19871  rolle  19874  cmvth  19875  mvth  19876  dvlip  19877  dvlipcn  19878  dvlip2  19879  c1liplem1  19880  c1lip2  19882  dvgt0lem1  19886  dvle  19891  dvivthlem1  19892  dvivth  19894  dvne0  19895  lhop1lem  19897  lhop1  19898  lhop2  19899  lhop  19900  dvcnvrelem1  19901  dvcnvrelem2  19902  dvcnvre  19903  dvcvx  19904  dvfsumle  19905  dvfsumge  19906  dvfsumabs  19907  dvfsumlem2  19911  dvfsumrlim  19915  ftc1a  19921  ftc1lem3  19922  ftc1lem6  19925  ftc1  19926  ftc1cn  19927  ftc2  19928  ftc2ditglem  19929  itgparts  19931  itgsubstlem  19932  itgsubst  19933  aacjcl  20244  aalioulem3  20251  taylthlem2  20290  taylth  20291  abelth2  20358  reeff1olem  20362  efcvx  20365  pilem3  20369  pige3  20425  recosf1o  20437  resinf1o  20438  dvrelog  20528  relogcn  20529  logcnlem5  20537  logcn  20538  dvloglem  20539  dvlog2lem  20543  logccv  20554  dvcxp1  20626  cxpcn3  20632  resqrcn  20633  loglesqr  20642  ssscongptld  20666  ressatans  20774  rlimcnp  20804  efrlim  20808  jensenlem1  20825  jensenlem2  20826  jensen  20827  amgm  20829  ftalem3  20857  basellem9  20871  efnnfsumcl  20885  efchtdvds  20942  lgsdchr  21132  dchrvmasumlem1  21189  dchrisum0lem3  21213  pntlem3  21303  readdsubgo  21941  circgrp  21962  ipasslem7  22337  rexdiv  24172  fsumrp0cl  24217  rebase  24269  re0g  24273  unitsscn  24294  rmulccn  24314  raddcn  24315  xrge0iifhom  24323  lmlimxrge0  24334  recms  24343  reust  24344  rezh  24355  rrhre  24387  esumpfinvallem  24464  esumpfinval  24465  esumpfinvalf  24466  esumcvg  24476  lgamgulmlem2  24814  cvxpcon  24929  cvxscon  24930  rescon  24933  fprodrecl  25279  fprodrpcl  25282  rerisefaccl  25333  refallfaccl  25334  rprisefaccl  25339  mblfinlem2  26244  mbfresfi  26253  ftc1cnnclem  26278  ftc1cnnc  26279  ftc1anclem3  26282  ftc1anclem5  26284  ftc1anclem7  26286  ftc1anclem8  26287  ftc1anc  26288  ftc2nc  26289  dvreasin  26290  dvreacos  26291  areacirclem1  26292  areacirclem2  26293  areacirclem3  26294  areacirclem4  26295  areacirc  26297  ivthALT  26338  repwsmet  26543  rrnequiv  26544  rrntotbnd  26545  reheibor  26548  iccbnd  26549  ssrecnpr  27514  sblpnf  27516  lhe4.4ex1a  27523  refsumcn  27677  climreeq  27715  dvcosre  27717  itgsin0pilem1  27720  ibliccsinexp  27721  iblioosinexp  27723  itgsinexplem1  27724  itgsinexp  27725  wallispilem2  27791
  Copyright terms: Public domain W3C validator