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

Theorem reseq1d 5933
Description: Equality deduction for restrictions. (Contributed by NM, 21-Oct-2014.)
Hypothesis
Ref Expression
reseqd.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
reseq1d (𝜑 → (𝐴𝐶) = (𝐵𝐶))

Proof of Theorem reseq1d
StepHypRef Expression
1 reseqd.1 . 2 (𝜑𝐴 = 𝐵)
2 reseq1 5928 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  cres 5633
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 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3407  df-in 3916  df-res 5643
This theorem is referenced by:  reseq12d  5935  fun2ssres  6542  funcnvres2  6577  fresin  6707  fresaunres2  6710  offres  7907  itunifval  10286  hsmex  10302  gruima  10672  fseq1p1m1  13444  ltweuz  13795  rlimres  15375  lo1res  15376  lo1resb  15381  rlimresb  15382  o1resb  15383  bitsf1ocnv  16259  fsets  16976  setsres  16985  setscom  16987  sscres  17641  resfval2  17714  estrres  17962  symgvalstruct  19110  symgvalstructOLD  19111  gsumzres  19615  gsumzsplit  19633  gsum2dlem2  19677  dpjidcl  19766  pgpfaclem1  19789  pwssplit2  20444  pwssplit3  20445  znle2  20883  phssip  20985  mamures  21661  ofco2  21722  mdetunilem9  21891  mdetmul  21894  smadiadetglem1  21942  smadiadetglem2  21943  tmdgsum  23368  tsmsval2  23403  tsmsres  23417  tsmssplit  23425  imasdsf1olem  23648  tmslem  23759  tmslemOLD  23760  sranlm  23970  cmssmscld  24636  srabn  24646  cmscsscms  24659  mbflimsup  24952  dvres  25197  dvres3a  25200  dvmptresicc  25202  dvnres  25217  cpnres  25223  dvcmul  25230  dvcmulf  25231  dvcobr  25232  dvmptres3  25242  dvmptres2  25248  dvcnvlem  25262  dvlip2  25281  ftc2ditglem  25331  itgpowd  25336  aannenlem1  25610  eff1olem  25826  resqrtcn  26024  sqrtcn  26025  rlimcnp2  26238  jensenlem2  26259  ex-res  29171  rabfodom  31217  resf1o  31429  tocycfvres1  31741  tocycfvres2  31742  cycpmconjvlem  31772  cycpmconjslem2  31786  cyc3conja  31788  lbsdiflsp0  32092  submatres  32148  zhmnrg  32309  indf1ofs  32386  carsggect  32679  fibp1  32762  actfunsnf1o  32978  cvmliftlem10  33649  cvmlift2lem6  33663  cvmlift2lem12  33669  satf  33708  poimirlem3  35967  ftc1anclem8  36044  ftc2nc  36046  cocnv  36070  cnpwstotbnd  36142  drngoi  36296  eldioph2  40919  dvsconst  42343  disjf1o  43130  cncfmptss  43538  limsupresuz  43654  liminfresuz  43735  itgsinexplem1  43905  itgcoscmulx  43920  itgiccshift  43931  itgperiod  43932  dirkeritg  44053  dirkercncflem2  44055  dirkercncflem4  44057  fourierdlem16  44074  fourierdlem21  44079  fourierdlem22  44080  fourierdlem28  44086  fourierdlem42  44100  fourierdlem78  44135  fourierdlem81  44138  fourierdlem83  44140  fourierdlem84  44141  fourierdlem90  44147  fourierdlem93  44150  fourierdlem103  44160  fourierdlem104  44161  sge0resrnlem  44352  ismeannd  44416  0ome  44478  hoidmvlelem3  44546  hoidmvlelem4  44547  funcrngcsetc  45996  funcringcsetc  46033  rhmsubclem1  46084  rhmsubcALTVlem1  46102  aacllem  46944
  Copyright terms: Public domain W3C validator