Theorem reseq1d 5937

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

Syntax hints:   → wi 4   = wceq 1547   ↾ cres 5627

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 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-in 3897  df-res 5637

This theorem is referenced by:  reseq12d  5939  fun2ssres  6537  funcnvres2  6572  fresin  6703  fresaunres2  6706  offres  7932  itunifval  10336  hsmex  10352  gruima  10723  fseq1p1m1  13550  ltweuz  13921  rlimres  15518  lo1res  15519  lo1resb  15524  rlimresb  15525  o1resb  15526  bitsf1ocnv  16411  fsets  17137  setsres  17146  setscom  17148  sscres  17788  resfval2  17858  estrres  18103  symgvalstruct  19370  gsumzres  19882  gsumzsplit  19900  gsum2dlem2  19944  dpjidcl  20033  pgpfaclem1  20056  funcrngcsetc  20619  funcringcsetc  20653  rhmsubclem1  20664  pwssplit2  21057  pwssplit3  21058  znle2  21535  phssip  21640  mamures  22387  ofco2  22441  mdetunilem9  22610  mdetmul  22613  smadiadetglem1  22661  smadiadetglem2  22662  tmdgsum  24085  tsmsval2  24120  tsmsres  24134  tsmssplit  24142  imasdsf1olem  24363  tmslem  24472  sranlm  24674  cmssmscld  25342  srabn  25352  cmscsscms  25365  mbflimsup  25658  dvres  25903  dvres3a  25906  dvmptresicc  25908  dvnres  25923  cpnres  25929  dvcmul  25936  dvcmulf  25937  dvcobr  25938  dvmptres3  25948  dvmptres2  25954  dvcnvlem  25968  dvlip2  25987  ftc2ditglem  26037  itgpowd  26042  aannenlem1  26319  eff1olem  26537  resqrtcn  26738  sqrtcn  26739  rlimcnp2  26955  jensenlem2  26976  ex-res  30536  rabfodom  32600  padct  32817  resf1o  32829  indf1ofs  32952  tocycfvres1  33198  tocycfvres2  33199  cycpmconjvlem  33229  cycpmconjslem2  33243  cyc3conja  33245  gsumind  33435  ply1gsumz  33689  evlextv  33733  lbsdiflsp0  33817  submatres  33997  zhmnrg  34156  carsggect  34509  fibp1  34592  actfunsnf1o  34795  cvmliftlem10  35529  cvmlift2lem6  35543  cvmlift2lem12  35549  satf  35588  poimirlem3  37997  ftc1anclem8  38074  ftc2nc  38076  cocnv  38099  cnpwstotbnd  38171  drngoi  38325  aks6d1c6lem2  42663  aks6d1c6lem4  42665  eldioph2  43218  dvsconst  44781  disjf1o  45645  cncfmptss  46039  limsupresuz  46153  liminfresuz  46234  itgsinexplem1  46404  itgcoscmulx  46419  itgiccshift  46430  itgperiod  46431  dirkeritg  46552  dirkercncflem2  46554  dirkercncflem4  46556  fourierdlem16  46573  fourierdlem21  46578  fourierdlem22  46579  fourierdlem28  46585  fourierdlem42  46599  fourierdlem78  46634  fourierdlem81  46637  fourierdlem83  46639  fourierdlem84  46640  fourierdlem90  46646  fourierdlem93  46649  fourierdlem103  46659  fourierdlem104  46660  sge0resrnlem  46853  ismeannd  46917  0ome  46979  hoidmvlelem3  47047  hoidmvlelem4  47048  rhmsubcALTVlem1  48779  aacllem  50298