Theorem reseq1d 5949

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

Syntax hints:   → wi 4   = wceq 1540   ↾ cres 5640

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-in 3921  df-res 5650

This theorem is referenced by:  reseq12d  5951  fun2ssres  6561  funcnvres2  6596  fresin  6729  fresaunres2  6732  offres  7962  itunifval  10369  hsmex  10385  gruima  10755  fseq1p1m1  13559  ltweuz  13926  rlimres  15524  lo1res  15525  lo1resb  15530  rlimresb  15531  o1resb  15532  bitsf1ocnv  16414  fsets  17139  setsres  17148  setscom  17150  sscres  17785  resfval2  17855  estrres  18100  symgvalstruct  19327  gsumzres  19839  gsumzsplit  19857  gsum2dlem2  19901  dpjidcl  19990  pgpfaclem1  20013  funcrngcsetc  20549  funcringcsetc  20583  rhmsubclem1  20594  pwssplit2  20967  pwssplit3  20968  znle2  21463  phssip  21567  mamures  22284  ofco2  22338  mdetunilem9  22507  mdetmul  22510  smadiadetglem1  22558  smadiadetglem2  22559  tmdgsum  23982  tsmsval2  24017  tsmsres  24031  tsmssplit  24039  imasdsf1olem  24261  tmslem  24370  sranlm  24572  cmssmscld  25250  srabn  25260  cmscsscms  25273  mbflimsup  25567  dvres  25812  dvres3a  25815  dvmptresicc  25817  dvnres  25833  cpnres  25839  dvcmul  25847  dvcmulf  25848  dvcobr  25849  dvcobrOLD  25850  dvmptres3  25860  dvmptres2  25866  dvcnvlem  25880  dvlip2  25900  ftc2ditglem  25952  itgpowd  25957  aannenlem1  26236  eff1olem  26457  resqrtcn  26659  sqrtcn  26660  rlimcnp2  26876  jensenlem2  26898  ex-res  30370  rabfodom  32434  resf1o  32653  indf1ofs  32789  tocycfvres1  33067  tocycfvres2  33068  cycpmconjvlem  33098  cycpmconjslem2  33112  cyc3conja  33114  ply1gsumz  33564  lbsdiflsp0  33622  submatres  33796  zhmnrg  33955  carsggect  34309  fibp1  34392  actfunsnf1o  34595  cvmliftlem10  35281  cvmlift2lem6  35295  cvmlift2lem12  35301  satf  35340  poimirlem3  37617  ftc1anclem8  37694  ftc2nc  37696  cocnv  37719  cnpwstotbnd  37791  drngoi  37945  aks6d1c6lem2  42159  aks6d1c6lem4  42161  eldioph2  42750  dvsconst  44319  disjf1o  45185  cncfmptss  45585  limsupresuz  45701  liminfresuz  45782  itgsinexplem1  45952  itgcoscmulx  45967  itgiccshift  45978  itgperiod  45979  dirkeritg  46100  dirkercncflem2  46102  dirkercncflem4  46104  fourierdlem16  46121  fourierdlem21  46126  fourierdlem22  46127  fourierdlem28  46133  fourierdlem42  46147  fourierdlem78  46182  fourierdlem81  46185  fourierdlem83  46187  fourierdlem84  46188  fourierdlem90  46194  fourierdlem93  46197  fourierdlem103  46207  fourierdlem104  46208  sge0resrnlem  46401  ismeannd  46465  0ome  46527  hoidmvlelem3  46595  hoidmvlelem4  46596  rhmsubcALTVlem1  48269  aacllem  49790