Theorem reseq1d 5981

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-in 3956  df-res 5689

This theorem is referenced by:  reseq12d  5983  fun2ssres  6594  funcnvres2  6629  fresin  6761  fresaunres2  6764  offres  7970  itunifval  10411  hsmex  10427  gruima  10797  fseq1p1m1  13575  ltweuz  13926  rlimres  15502  lo1res  15503  lo1resb  15508  rlimresb  15509  o1resb  15510  bitsf1ocnv  16385  fsets  17102  setsres  17111  setscom  17113  sscres  17770  resfval2  17843  estrres  18091  symgvalstruct  19264  symgvalstructOLD  19265  gsumzres  19777  gsumzsplit  19795  gsum2dlem2  19839  dpjidcl  19928  pgpfaclem1  19951  pwssplit2  20671  pwssplit3  20672  znle2  21109  phssip  21211  mamures  21892  ofco2  21953  mdetunilem9  22122  mdetmul  22125  smadiadetglem1  22173  smadiadetglem2  22174  tmdgsum  23599  tsmsval2  23634  tsmsres  23648  tsmssplit  23656  imasdsf1olem  23879  tmslem  23990  tmslemOLD  23991  sranlm  24201  cmssmscld  24867  srabn  24877  cmscsscms  24890  mbflimsup  25183  dvres  25428  dvres3a  25431  dvmptresicc  25433  dvnres  25448  cpnres  25454  dvcmul  25461  dvcmulf  25462  dvcobr  25463  dvmptres3  25473  dvmptres2  25479  dvcnvlem  25493  dvlip2  25512  ftc2ditglem  25562  itgpowd  25567  aannenlem1  25841  eff1olem  26057  resqrtcn  26257  sqrtcn  26258  rlimcnp2  26471  jensenlem2  26492  ex-res  29694  rabfodom  31743  resf1o  31955  tocycfvres1  32269  tocycfvres2  32270  cycpmconjvlem  32300  cycpmconjslem2  32314  cyc3conja  32316  ply1gsumz  32669  lbsdiflsp0  32711  submatres  32786  zhmnrg  32947  indf1ofs  33024  carsggect  33317  fibp1  33400  actfunsnf1o  33616  cvmliftlem10  34285  cvmlift2lem6  34299  cvmlift2lem12  34305  satf  34344  gg-dvcobr  35176  poimirlem3  36491  ftc1anclem8  36568  ftc2nc  36570  cocnv  36593  cnpwstotbnd  36665  drngoi  36819  eldioph2  41500  dvsconst  43089  disjf1o  43889  cncfmptss  44303  limsupresuz  44419  liminfresuz  44500  itgsinexplem1  44670  itgcoscmulx  44685  itgiccshift  44696  itgperiod  44697  dirkeritg  44818  dirkercncflem2  44820  dirkercncflem4  44822  fourierdlem16  44839  fourierdlem21  44844  fourierdlem22  44845  fourierdlem28  44851  fourierdlem42  44865  fourierdlem78  44900  fourierdlem81  44903  fourierdlem83  44905  fourierdlem84  44906  fourierdlem90  44912  fourierdlem93  44915  fourierdlem103  44925  fourierdlem104  44926  sge0resrnlem  45119  ismeannd  45183  0ome  45245  hoidmvlelem3  45313  hoidmvlelem4  45314  funcrngcsetc  46896  funcringcsetc  46933  rhmsubclem1  46984  rhmsubcALTVlem1  47002  aacllem  47848