Theorem reseq1d 5945

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

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

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-in 3910  df-res 5644

This theorem is referenced by:  reseq12d  5947  fun2ssres  6545  funcnvres2  6580  fresin  6711  fresaunres2  6714  offres  7937  itunifval  10338  hsmex  10354  gruima  10725  fseq1p1m1  13526  ltweuz  13896  rlimres  15493  lo1res  15494  lo1resb  15499  rlimresb  15500  o1resb  15501  bitsf1ocnv  16383  fsets  17108  setsres  17117  setscom  17119  sscres  17759  resfval2  17829  estrres  18074  symgvalstruct  19338  gsumzres  19850  gsumzsplit  19868  gsum2dlem2  19912  dpjidcl  20001  pgpfaclem1  20024  funcrngcsetc  20585  funcringcsetc  20619  rhmsubclem1  20630  pwssplit2  21024  pwssplit3  21025  znle2  21520  phssip  21625  mamures  22353  ofco2  22407  mdetunilem9  22576  mdetmul  22579  smadiadetglem1  22627  smadiadetglem2  22628  tmdgsum  24051  tsmsval2  24086  tsmsres  24100  tsmssplit  24108  imasdsf1olem  24329  tmslem  24438  sranlm  24640  cmssmscld  25318  srabn  25328  cmscsscms  25341  mbflimsup  25635  dvres  25880  dvres3a  25883  dvmptresicc  25885  dvnres  25901  cpnres  25907  dvcmul  25915  dvcmulf  25916  dvcobr  25917  dvcobrOLD  25918  dvmptres3  25928  dvmptres2  25934  dvcnvlem  25948  dvlip2  25968  ftc2ditglem  26020  itgpowd  26025  aannenlem1  26304  eff1olem  26525  resqrtcn  26727  sqrtcn  26728  rlimcnp2  26944  jensenlem2  26966  ex-res  30528  rabfodom  32591  resf1o  32819  indf1ofs  32958  tocycfvres1  33203  tocycfvres2  33204  cycpmconjvlem  33234  cycpmconjslem2  33248  cyc3conja  33250  gsumind  33437  ply1gsumz  33691  evlextv  33718  lbsdiflsp0  33803  submatres  33983  zhmnrg  34142  carsggect  34495  fibp1  34578  actfunsnf1o  34781  cvmliftlem10  35507  cvmlift2lem6  35521  cvmlift2lem12  35527  satf  35566  poimirlem3  37868  ftc1anclem8  37945  ftc2nc  37947  cocnv  37970  cnpwstotbnd  38042  drngoi  38196  aks6d1c6lem2  42535  aks6d1c6lem4  42537  eldioph2  43113  dvsconst  44680  disjf1o  45544  cncfmptss  45941  limsupresuz  46055  liminfresuz  46136  itgsinexplem1  46306  itgcoscmulx  46321  itgiccshift  46332  itgperiod  46333  dirkeritg  46454  dirkercncflem2  46456  dirkercncflem4  46458  fourierdlem16  46475  fourierdlem21  46480  fourierdlem22  46481  fourierdlem28  46487  fourierdlem42  46501  fourierdlem78  46536  fourierdlem81  46539  fourierdlem83  46541  fourierdlem84  46542  fourierdlem90  46548  fourierdlem93  46551  fourierdlem103  46561  fourierdlem104  46562  sge0resrnlem  46755  ismeannd  46819  0ome  46881  hoidmvlelem3  46949  hoidmvlelem4  46950  rhmsubcALTVlem1  48635  aacllem  50154