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  29725  rabfodom  31774  resf1o  31986  tocycfvres1  32300  tocycfvres2  32301  cycpmconjvlem  32331  cycpmconjslem2  32345  cyc3conja  32347  ply1gsumz  32700  lbsdiflsp0  32742  submatres  32817  zhmnrg  32978  indf1ofs  33055  carsggect  33348  fibp1  33431  actfunsnf1o  33647  cvmliftlem10  34316  cvmlift2lem6  34330  cvmlift2lem12  34336  satf  34375  gg-dvcobr  35207  poimirlem3  36539  ftc1anclem8  36616  ftc2nc  36618  cocnv  36641  cnpwstotbnd  36713  drngoi  36867  eldioph2  41548  dvsconst  43137  disjf1o  43937  cncfmptss  44351  limsupresuz  44467  liminfresuz  44548  itgsinexplem1  44718  itgcoscmulx  44733  itgiccshift  44744  itgperiod  44745  dirkeritg  44866  dirkercncflem2  44868  dirkercncflem4  44870  fourierdlem16  44887  fourierdlem21  44892  fourierdlem22  44893  fourierdlem28  44899  fourierdlem42  44913  fourierdlem78  44948  fourierdlem81  44951  fourierdlem83  44953  fourierdlem84  44954  fourierdlem90  44960  fourierdlem93  44963  fourierdlem103  44973  fourierdlem104  44974  sge0resrnlem  45167  ismeannd  45231  0ome  45293  hoidmvlelem3  45361  hoidmvlelem4  45362  funcrngcsetc  46944  funcringcsetc  46981  rhmsubclem1  47032  rhmsubcALTVlem1  47050  aacllem  47896