Theorem reseq1d 5888

Description: Equality deduction for restrictions. (Contributed by NM, 21-Oct-2014.)

Hypothesis

Ref	Expression
reseqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
reseq1d	⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))

Proof of Theorem reseq1d

Step	Hyp	Ref	Expression
1		reseqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		reseq1 5883	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))

Syntax hints:   → wi 4   = wceq 1542   ↾ cres 5591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-rab 3075  df-in 3899  df-res 5601

This theorem is referenced by:  reseq12d  5890  fun2ssres  6476  funcnvres2  6511  fresin  6640  fresaunres2  6643  offres  7817  trpredeq1  9465  trpredeq2  9466  trpredeq3  9467  itunifval  10171  hsmex  10187  gruima  10557  fseq1p1m1  13327  ltweuz  13677  rlimres  15263  lo1res  15264  lo1resb  15269  rlimresb  15270  o1resb  15271  bitsf1ocnv  16147  fsets  16866  setsres  16875  setscom  16877  sscres  17531  resfval2  17604  estrres  17852  symgvalstruct  19000  symgvalstructOLD  19001  gsumzres  19506  gsumzsplit  19524  gsum2dlem2  19568  dpjidcl  19657  pgpfaclem1  19680  pwssplit2  20318  pwssplit3  20319  znle2  20757  phssip  20859  mamures  21535  ofco2  21596  mdetunilem9  21765  mdetmul  21768  smadiadetglem1  21816  smadiadetglem2  21817  tmdgsum  23242  tsmsval2  23277  tsmsres  23291  tsmssplit  23299  imasdsf1olem  23522  tmslem  23633  tmslemOLD  23634  sranlm  23844  cmssmscld  24510  srabn  24520  cmscsscms  24533  mbflimsup  24826  dvres  25071  dvres3a  25074  dvmptresicc  25076  dvnres  25091  cpnres  25097  dvcmul  25104  dvcmulf  25105  dvcobr  25106  dvmptres3  25116  dvmptres2  25122  dvcnvlem  25136  dvlip2  25155  ftc2ditglem  25205  itgpowd  25210  aannenlem1  25484  eff1olem  25700  resqrtcn  25898  sqrtcn  25899  rlimcnp2  26112  jensenlem2  26133  ex-res  28799  rabfodom  30845  resf1o  31059  tocycfvres1  31371  tocycfvres2  31372  cycpmconjvlem  31402  cycpmconjslem2  31416  cyc3conja  31418  lbsdiflsp0  31701  submatres  31750  zhmnrg  31911  indf1ofs  31988  carsggect  32279  fibp1  32362  actfunsnf1o  32578  cvmliftlem10  33250  cvmlift2lem6  33264  cvmlift2lem12  33270  satf  33309  poimirlem3  35774  ftc1anclem8  35851  ftc2nc  35853  cocnv  35877  cnpwstotbnd  35949  drngoi  36103  eldioph2  40579  dvsconst  41916  disjf1o  42697  cncfmptss  43097  limsupresuz  43213  liminfresuz  43294  itgsinexplem1  43464  itgcoscmulx  43479  itgiccshift  43490  itgperiod  43491  dirkeritg  43612  dirkercncflem2  43614  dirkercncflem4  43616  fourierdlem16  43633  fourierdlem21  43638  fourierdlem22  43639  fourierdlem28  43645  fourierdlem42  43659  fourierdlem78  43694  fourierdlem81  43697  fourierdlem83  43699  fourierdlem84  43700  fourierdlem90  43706  fourierdlem93  43709  fourierdlem103  43719  fourierdlem104  43720  sge0resrnlem  43910  ismeannd  43974  0ome  44036  hoidmvlelem3  44104  hoidmvlelem4  44105  funcrngcsetc  45523  funcringcsetc  45560  rhmsubclem1  45611  rhmsubcALTVlem1  45629  aacllem  46472