Theorem reseq1d 5990

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 5985	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))

Syntax hints:   → wi 4   = wceq 1534   ↾ cres 5686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420  df-in 3954  df-res 5696

This theorem is referenced by:  reseq12d  5992  fun2ssres  6606  funcnvres2  6641  fresin  6773  fresaunres2  6776  offres  7999  itunifval  10461  hsmex  10477  gruima  10847  fseq1p1m1  13631  ltweuz  13983  rlimres  15562  lo1res  15563  lo1resb  15568  rlimresb  15569  o1resb  15570  bitsf1ocnv  16446  fsets  17173  setsres  17182  setscom  17184  sscres  17841  resfval2  17914  estrres  18165  symgvalstruct  19396  symgvalstructOLD  19397  gsumzres  19909  gsumzsplit  19927  gsum2dlem2  19971  dpjidcl  20060  pgpfaclem1  20083  funcrngcsetc  20620  funcringcsetc  20654  rhmsubclem1  20665  pwssplit2  21040  pwssplit3  21041  znle2  21553  phssip  21656  mamures  22391  ofco2  22447  mdetunilem9  22616  mdetmul  22619  smadiadetglem1  22667  smadiadetglem2  22668  tmdgsum  24093  tsmsval2  24128  tsmsres  24142  tsmssplit  24150  imasdsf1olem  24373  tmslem  24484  tmslemOLD  24485  sranlm  24695  cmssmscld  25372  srabn  25382  cmscsscms  25395  mbflimsup  25689  dvres  25934  dvres3a  25937  dvmptresicc  25939  dvnres  25955  cpnres  25961  dvcmul  25969  dvcmulf  25970  dvcobr  25971  dvcobrOLD  25972  dvmptres3  25982  dvmptres2  25988  dvcnvlem  26002  dvlip2  26022  ftc2ditglem  26074  itgpowd  26079  aannenlem1  26359  eff1olem  26578  resqrtcn  26780  sqrtcn  26781  rlimcnp2  26997  jensenlem2  27019  ex-res  30377  rabfodom  32434  resf1o  32646  tocycfvres1  32990  tocycfvres2  32991  cycpmconjvlem  33021  cycpmconjslem2  33035  cyc3conja  33037  ply1gsumz  33468  lbsdiflsp0  33523  submatres  33623  zhmnrg  33784  indf1ofs  33861  carsggect  34154  fibp1  34237  actfunsnf1o  34452  cvmliftlem10  35124  cvmlift2lem6  35138  cvmlift2lem12  35144  satf  35183  poimirlem3  37326  ftc1anclem8  37403  ftc2nc  37405  cocnv  37428  cnpwstotbnd  37500  drngoi  37654  aks6d1c6lem2  41871  aks6d1c6lem4  41873  eldioph2  42437  dvsconst  44022  disjf1o  44816  cncfmptss  45226  limsupresuz  45342  liminfresuz  45423  itgsinexplem1  45593  itgcoscmulx  45608  itgiccshift  45619  itgperiod  45620  dirkeritg  45741  dirkercncflem2  45743  dirkercncflem4  45745  fourierdlem16  45762  fourierdlem21  45767  fourierdlem22  45768  fourierdlem28  45774  fourierdlem42  45788  fourierdlem78  45823  fourierdlem81  45826  fourierdlem83  45828  fourierdlem84  45829  fourierdlem90  45835  fourierdlem93  45838  fourierdlem103  45848  fourierdlem104  45849  sge0resrnlem  46042  ismeannd  46106  0ome  46168  hoidmvlelem3  46236  hoidmvlelem4  46237  rhmsubcALTVlem1  47676  aacllem  48567