Theorem reseq1d 5996

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-in 3958  df-res 5697

This theorem is referenced by:  reseq12d  5998  fun2ssres  6611  funcnvres2  6646  fresin  6777  fresaunres2  6780  offres  8008  itunifval  10456  hsmex  10472  gruima  10842  fseq1p1m1  13638  ltweuz  14002  rlimres  15594  lo1res  15595  lo1resb  15600  rlimresb  15601  o1resb  15602  bitsf1ocnv  16481  fsets  17206  setsres  17215  setscom  17217  sscres  17867  resfval2  17938  estrres  18184  symgvalstruct  19414  symgvalstructOLD  19415  gsumzres  19927  gsumzsplit  19945  gsum2dlem2  19989  dpjidcl  20078  pgpfaclem1  20101  funcrngcsetc  20640  funcringcsetc  20674  rhmsubclem1  20685  pwssplit2  21059  pwssplit3  21060  znle2  21572  phssip  21676  mamures  22401  ofco2  22457  mdetunilem9  22626  mdetmul  22629  smadiadetglem1  22677  smadiadetglem2  22678  tmdgsum  24103  tsmsval2  24138  tsmsres  24152  tsmssplit  24160  imasdsf1olem  24383  tmslem  24494  tmslemOLD  24495  sranlm  24705  cmssmscld  25384  srabn  25394  cmscsscms  25407  mbflimsup  25701  dvres  25946  dvres3a  25949  dvmptresicc  25951  dvnres  25967  cpnres  25973  dvcmul  25981  dvcmulf  25982  dvcobr  25983  dvcobrOLD  25984  dvmptres3  25994  dvmptres2  26000  dvcnvlem  26014  dvlip2  26034  ftc2ditglem  26086  itgpowd  26091  aannenlem1  26370  eff1olem  26590  resqrtcn  26792  sqrtcn  26793  rlimcnp2  27009  jensenlem2  27031  ex-res  30460  rabfodom  32524  resf1o  32741  indf1ofs  32851  tocycfvres1  33130  tocycfvres2  33131  cycpmconjvlem  33161  cycpmconjslem2  33175  cyc3conja  33177  ply1gsumz  33619  lbsdiflsp0  33677  submatres  33805  zhmnrg  33966  carsggect  34320  fibp1  34403  actfunsnf1o  34619  cvmliftlem10  35299  cvmlift2lem6  35313  cvmlift2lem12  35319  satf  35358  poimirlem3  37630  ftc1anclem8  37707  ftc2nc  37709  cocnv  37732  cnpwstotbnd  37804  drngoi  37958  aks6d1c6lem2  42172  aks6d1c6lem4  42174  eldioph2  42773  dvsconst  44349  disjf1o  45196  cncfmptss  45602  limsupresuz  45718  liminfresuz  45799  itgsinexplem1  45969  itgcoscmulx  45984  itgiccshift  45995  itgperiod  45996  dirkeritg  46117  dirkercncflem2  46119  dirkercncflem4  46121  fourierdlem16  46138  fourierdlem21  46143  fourierdlem22  46144  fourierdlem28  46150  fourierdlem42  46164  fourierdlem78  46199  fourierdlem81  46202  fourierdlem83  46204  fourierdlem84  46205  fourierdlem90  46211  fourierdlem93  46214  fourierdlem103  46224  fourierdlem104  46225  sge0resrnlem  46418  ismeannd  46482  0ome  46544  hoidmvlelem3  46612  hoidmvlelem4  46613  rhmsubcALTVlem1  48197  aacllem  49320