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

Theorem reseq1d 5932
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 5927 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  cres 5632
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3406  df-in 3915  df-res 5642
This theorem is referenced by:  reseq12d  5934  fun2ssres  6541  funcnvres2  6576  fresin  6706  fresaunres2  6709  offres  7906  itunifval  10285  hsmex  10301  gruima  10671  fseq1p1m1  13443  ltweuz  13794  rlimres  15374  lo1res  15375  lo1resb  15380  rlimresb  15381  o1resb  15382  bitsf1ocnv  16258  fsets  16975  setsres  16984  setscom  16986  sscres  17640  resfval2  17713  estrres  17961  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  29183  rabfodom  31229  resf1o  31441  tocycfvres1  31753  tocycfvres2  31754  cycpmconjvlem  31784  cycpmconjslem2  31798  cyc3conja  31800  lbsdiflsp0  32104  submatres  32160  zhmnrg  32321  indf1ofs  32398  carsggect  32691  fibp1  32774  actfunsnf1o  32990  cvmliftlem10  33661  cvmlift2lem6  33675  cvmlift2lem12  33681  satf  33720  poimirlem3  35976  ftc1anclem8  36053  ftc2nc  36055  cocnv  36079  cnpwstotbnd  36151  drngoi  36305  eldioph2  40950  dvsconst  42374  disjf1o  43167  cncfmptss  43581  limsupresuz  43697  liminfresuz  43778  itgsinexplem1  43948  itgcoscmulx  43963  itgiccshift  43974  itgperiod  43975  dirkeritg  44096  dirkercncflem2  44098  dirkercncflem4  44100  fourierdlem16  44117  fourierdlem21  44122  fourierdlem22  44123  fourierdlem28  44129  fourierdlem42  44143  fourierdlem78  44178  fourierdlem81  44181  fourierdlem83  44183  fourierdlem84  44184  fourierdlem90  44190  fourierdlem93  44193  fourierdlem103  44203  fourierdlem104  44204  sge0resrnlem  44397  ismeannd  44461  0ome  44523  hoidmvlelem3  44591  hoidmvlelem4  44592  funcrngcsetc  46045  funcringcsetc  46082  rhmsubclem1  46133  rhmsubcALTVlem1  46151  aacllem  46993
  Copyright terms: Public domain W3C validator