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

Axiom ax-resscn 8790
Description: The real numbers are a subset of the complex numbers. Axiom 1 of 22 for real and complex numbers, justified by theorem axresscn 8766. (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 8732 . 2  class  RR
2 cc 8731 . 2  class  CC
31, 2wss 3154 1  wff  RR  C_  CC
Colors of variables: wff set class
This axiom is referenced by:  recn  8823  reex  8824  recni  8845  nnsscn  9747  nn0sscn  9966  qsscn  10323  reexpcl  11115  rpexpcl  11117  reexpclz  11118  expge0  11133  expge1  11134  rlimrecl  12049  abscn2  12067  recn2  12069  imcn2  12070  climabs  12072  climre  12074  climim  12075  rlimabs  12077  rlimre  12079  rlimim  12080  caurcvgr  12141  caucvgrlem2  12142  caurcvg  12144  fsumrecl  12202  fsumrpcl  12205  fsumge0  12248  fsumre  12261  fsumim  12262  reeff1  12395  nthruc  12524  remet  18291  tgioo2  18304  xrsdsre  18311  recld2  18315  reperf  18319  iitopon  18378  dfii3  18382  abscncf  18400  recncf  18401  imcncf  18402  abscncfALT  18418  cnmptre  18420  iimulcn  18431  icchmeo  18434  cnrehmeo  18446  evth  18452  evth2  18453  lebnumlem2  18455  lebnumii  18459  reparphti  18490  cphsqrcl  18615  resscdrg  18770  ishl2  18782  evthicc  18814  evthicc2  18815  ovolfsf  18826  volcn  18956  volivth  18957  ismbf  18980  cncombf  19008  cnmbf  19009  0plef  19022  itg1ge0  19036  i1faddlem  19043  i1fmul  19046  itg1addlem4  19049  i1fsub  19058  itg1sub  19059  mbfi1fseqlem5  19069  xrge0f  19081  itg20  19087  itg2const  19090  itg2mulc  19097  itg2addlem  19108  i1fibl  19157  itgitg1  19158  iblabslem  19177  iblabs  19178  bddmulibl  19188  recnprss  19249  dvcjbr  19293  dvfre  19295  dvnfre  19296  dvferm1  19327  dvferm2  19329  rolle  19332  cmvth  19333  mvth  19334  dvlip  19335  dvlipcn  19336  dvlip2  19337  c1liplem1  19338  c1lip2  19340  dvgt0lem1  19344  dvle  19349  dvivthlem1  19350  dvivth  19352  dvne0  19353  lhop1lem  19355  lhop1  19356  lhop2  19357  lhop  19358  dvcnvrelem1  19359  dvcnvrelem2  19360  dvcnvre  19361  dvcvx  19362  dvfsumle  19363  dvfsumge  19364  dvfsumabs  19365  dvfsumlem2  19369  dvfsumrlim  19373  ftc1a  19379  ftc1lem3  19380  ftc1lem6  19383  ftc1  19384  ftc1cn  19385  ftc2  19386  ftc2ditglem  19387  itgparts  19389  itgsubstlem  19390  itgsubst  19391  aacjcl  19702  aalioulem3  19709  taylthlem2  19748  taylth  19749  abelth2  19813  reeff1olem  19817  efcvx  19820  pilem3  19824  pige3  19880  recosf1o  19892  resinf1o  19893  dvrelog  19979  relogcn  19980  logcnlem5  19988  logcn  19989  dvloglem  19990  dvlog2lem  19994  logccv  20005  dvcxp1  20077  cxpcn3  20083  resqrcn  20084  loglesqr  20093  ssscongptld  20117  ressatans  20225  rlimcnp  20255  efrlim  20259  jensenlem1  20276  jensenlem2  20277  jensen  20278  amgm  20280  ftalem3  20307  basellem9  20321  efnnfsumcl  20335  efchtdvds  20392  lgsdchr  20582  dchrvmasumlem1  20639  dchrisum0lem3  20663  pntlem3  20753  readdsubgo  21013  circgrp  21034  ipasslem7  21407  cvxpcon  23178  cvxscon  23179  rescon  23182  claddrvr  25048  rnegvex2  25061  negveudr  25069  subclrvd  25074  clsmulrv  25083  divclrvd  25095  ivthALT  25658  repwsmet  25958  rrnequiv  25959  rrntotbnd  25960  reheibor  25963  iccbnd  25964  ssrecnpr  26937  sblpnf  26939  lhe4.4ex1a  26946  refsumcn  27101  climreeq  27139  dvcosre  27141  ibliccsinexp  27145  iblioosinexp  27147  itgsinexplem1  27148  itgsinexp  27149  wallispilem2  27215  wallispilem4  27217  wallispi  27219
  Copyright terms: Public domain W3C validator