MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reseq2d Structured version   Visualization version   GIF version

Theorem reseq2d 5942
Description: Equality deduction for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypothesis
Ref Expression
reseqd.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
reseq2d (𝜑 → (𝐶𝐴) = (𝐶𝐵))

Proof of Theorem reseq2d
StepHypRef Expression
1 reseqd.1 . 2 (𝜑𝐴 = 𝐵)
2 reseq2 5937 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  cres 5640
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3411  df-in 3922  df-opab 5173  df-xp 5644  df-res 5650
This theorem is referenced by:  reseq12d  5943  resresdm  6190  relresfld  6233  f1orescnv  6804  fococnv2  6815  fvn0ssdmfun  7030  fnressn  7109  fnsnsplit  7135  oprssov  7528  curry1  8041  curry2  8044  dftpos2  8179  frecseq123  8218  fpr3g  8221  frrlem1  8222  frrlem4  8225  frrlem12  8233  fpr2a  8238  wrecseq123OLD  8251  wfr3g  8258  wfrlem1OLD  8259  wfrlem4OLD  8263  wfrlem14OLD  8273  wfr2aOLD  8277  dfrecs3  8323  dfrecs3OLD  8324  tfrlem16  8344  tfr2ALT  8352  tfr3ALT  8353  on2recsov  8619  sbthlem4  9037  mapunen  9097  hartogslem1  9485  frr3g  9699  frr2  9703  axdc3lem2  10394  fseq1p1m1  13522  resunimafz0  14349  hashf1lem1  14360  hashf1lem1OLD  14361  relexp0g  14914  relexp0  14915  relexpsucnnr  14917  dfrtrcl2  14954  bpolylem  15938  setsval  17046  idfuval  17769  idfu2nd  17770  resf1st  17787  setcid  17979  catcisolem  18003  estrcid  18028  funcestrcsetclem5  18039  funcsetcestrclem5  18054  funcsetcestrclem7  18056  1stfval  18086  1stf2  18088  2ndfval  18089  2ndf2  18091  1stfcl  18092  2ndfcl  18093  curf2ndf  18143  hofcl  18155  isps  18464  cnvps  18474  isdir  18494  dirref  18497  tsrdir  18500  frmdval  18668  frmdplusg  18671  gsum2dlem2  19755  dprd2da  19828  dpjval  19842  ablfac1eulem  19858  ablfac1eu  19859  psrplusg  21365  opsrtoslem2  21479  mdetunilem3  21979  mdetunilem4  21980  mdetunilem9  21985  imacmp  22764  ptuncnv  23174  tgphaus  23484  tsmsres  23511  tsmsxplem1  23520  tsmsxplem2  23521  trust  23597  metreslem  23731  imasdsf1olem  23742  xmspropd  23842  mspropd  23843  imasf1oxms  23861  imasf1oms  23862  nmpropd2  23967  isngp2  23969  ngppropd  24009  tngngp2  24032  cphsscph  24631  cmspropd  24729  cmssmscld  24730  mbfres2  25025  limciun  25274  dvmptres3  25336  dvmptres2  25342  dvmptntr  25351  dvlipcn  25374  dvlip2  25375  c1liplem1  25376  dvgt0lem1  25382  lhop1lem  25393  dvcnvrelem1  25397  dvcvx  25400  ftc2ditglem  25425  wilthlem2  26434  dchrval  26598  dchrelbas2  26601  noresle  27061  nosupcbv  27066  nosupno  27067  nosupdm  27068  nosupfv  27070  nosupres  27071  nosupbnd1lem1  27072  nosupbnd1lem3  27074  nosupbnd1lem5  27076  nosupbnd1  27078  nosupbnd2  27080  noinfcbv  27081  noinfno  27082  noinfdm  27083  noinffv  27085  noinfres  27086  noinfbnd1lem3  27089  noinfbnd1lem5  27091  noinfbnd1  27093  noinfbnd2  27095  noetalem1  27105  norecov  27281  norec2ov  27291  egrsubgr  28267  pthdlem1  28756  eupthvdres  29221  eupth2lem3  29222  eupth2  29225  eucrct2eupth  29231  hhssablo  30247  hhssnvt  30249  hhsssh  30253  fnunres1  31566  fressupp  31645  resf1o  31689  gsummpt2d  31933  gsumpart  31939  symgcom  31976  tocycval  31999  tocycfv  32000  tocycf  32008  tocyc01  32009  cycpm2tr  32010  cycpmconjslem1  32045  cycpmconjslem2  32046  nsgqusf1o  32234  qtophaus  32457  esumcvg  32725  eulerpartlemn  33021  sseqp1  33035  signsvtn0  33222  ftc2re  33251  reprsuc  33268  bnj1385  33484  bnj1326  33678  bnj1321  33679  bnj1442  33701  bnj1450  33702  bnj1463  33707  bnj1529  33722  f1resfz0f1d  33744  pfxwlk  33757  pthhashvtx  33761  cvmliftlem5  33923  cvmliftlem7  33925  cvmliftlem10  33928  cvmliftlem11  33929  cvmliftlem15  33932  cvmlift2lem11  33947  cvmlift2lem12  33948  satffunlem1lem1  34036  satffunlem2lem1  34038  eldm3  34373  funsseq  34381  finixpnum  36092  poimirlem3  36110  poimirlem4  36111  poimirlem9  36116  sdclem2  36230  prdsbnd2  36283  isdivrngo  36438  drngoi  36439  elrefsymrels2  37060  eleqvrels2  37083  dibffval  39632  hdmapffval  40318  hdmapfval  40319  eldiophb  41109  diophrw  41111  diophin  41124  ofoafg  41699  resisoeq45d  41766  rclexi  41961  rtrclex  41963  rtrclexi  41967  cnvrcl0  41971  dfrtrcl5  41975  dfrcl2  42020  fvmptiunrelexplb0da  42031  sblpnf  42664  fresin2  43463  limsupresuz  44018  limsupvaluz  44023  limsupvaluz2  44053  supcnvlimsup  44055  climrescn  44063  liminfresuz  44099  cncfuni  44201  dvresntr  44233  dvbdfbdioolem1  44243  itgiccshift  44295  itgperiod  44296  dirkercncflem2  44419  fourierdlem46  44467  fourierdlem48  44469  fourierdlem49  44470  fourierdlem58  44479  fourierdlem72  44493  fourierdlem74  44495  fourierdlem75  44496  fourierdlem81  44502  fourierdlem88  44509  fourierdlem89  44510  fourierdlem90  44511  fourierdlem91  44512  fourierdlem92  44513  fourierdlem103  44524  fourierdlem104  44525  fourierdlem112  44533  fouriersw  44546  voncmpl  44936  funcoressn  45350  funressnmo  45354  f1cof1blem  45382  funfocofob  45384  funressndmafv2rn  45529  f1oresf1orab  45595  isomgreqve  46091  idfusubc0  46237  idfusubc  46238  rngcval  46334  rnghmsubcsetclem1  46347  rngccat  46350  rngcid  46351  rngcidALTV  46363  rngcifuestrc  46369  funcrngcsetc  46370  funcrngcsetcALT  46371  ringcval  46380  rhmsubcsetclem1  46393  ringccat  46396  ringcid  46397  rhmsubcrngclem1  46399  rhmsubcrngc  46401  funcringcsetc  46407  funcringcsetcALTV2lem5  46412  ringcidALTV  46426  funcringcsetclem5ALTV  46435  rhmsubc  46462  rhmsubcALTVlem3  46478  itcoval  46821  itcoval0mpt  46826  itcovalendof  46829  aacllem  47322
  Copyright terms: Public domain W3C validator