Theorem reseq1i 5959

Description: Equality inference for restrictions. (Contributed by NM, 21-Oct-2014.)

Hypothesis

Ref	Expression
reseqi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
reseq1i	⊢ (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)

Proof of Theorem reseq1i

Step	Hyp	Ref	Expression
1		reseqi.1	. 2 ⊢ 𝐴 = 𝐵
2		reseq1 5957	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)

Syntax hints:   = wceq 1559   ↾ cres 5647

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-in 3911  df-res 5657

This theorem is referenced by:  reseq12i  5961  resindmOLD  6015  resmpt  6023  resmpt3  6024  resmptf  6025  elimampt  6029  opabresid  6036  rescnvcnv  6187  coires1  6248  fnunres2  6630  fresaunres1  6733  fcoi1  6734  fninfp  7154  fvsnun1  7162  fvsnun2  7163  resoprab  7510  resmpo  7512  elimampo  7529  elrnmpores  7530  ofmres  7961  f1stres  7990  f2ndres  7991  df1st2  8072  df2nd2  8073  fsplitfpar  8092  dftpos2  8218  frrlem12  8273  tfr2a  8361  tfr2b  8362  rdgseg  8388  frsucmpt2  8406  seqomlem2  8417  seqomlem3  8418  seqomlem4  8419  domss2  9104  dffi3  9374  axdc  10475  fpwwe2lem12  10597  seqval  14022  hashgval  14343  hashinf  14345  submefmnd  18912  pgrpsubgsymg  19432  gsumzunsnd  19979  ablfac1b  20095  zzngim  21584  pmatcollpw3lem  22823  txflf  24046  xmsxmet2  24499  msmet2  24500  tmsxpsmopn  24577  isngp2  24637  subgnm  24673  tngngp2  24692  cnfldms  24815  msdcn  24882  oprpiece1res1  24993  oprpiece1res2  24994  isncvsngp  25191  cncms  25397  cnfldcusp  25399  reust  25423  minveclem3a  25469  dvreslem  25951  dvres2lem  25952  dvmptresicc  25958  dvcmulf  25987  mdegfval  26102  psercn  26466  abelth  26481  efcvx  26489  efifo  26589  dfrelog  26607  dvrelog  26679  dvlog  26693  efopnlem2  26699  dvatan  26977  dchrisumlem1  27530  noetasuplem2  27775  noetasuplem3  27776  noetasuplem4  27777  noetainflem2  27779  wlknwwlksnbij  30034  df1stres  32856  df2ndres  32857  padct  32870  ressplusf  33102  ressnm  33103  gsummpt2d  33190  cycpmrn  33284  tocyccntz  33285  cycpmconjslem2  33296  qusima  33555  qqhcn  34249  cnrrext  34268  rrhre  34279  esumcvg  34344  dya2icoseg2  34536  eulerpartgbij  34630  satf0  35686  neibastop2  36685  mptsnunlem  37796  icorempo  37809  poimirlem3  38086  mbfposadd  38130  ftc1anclem3  38158  dvasin  38167  dvacos  38168  prdsbnd2  38258  repwsmet  38297  rrnequiv  38298  inres2  38710  xrnres  38888  xrnres2  38889  xrnres3  38890  diophin  43317  eldioph4b  43352  dnnumch1  43585  aomclem6  43600  radcnvrat  44854  lhe4.4ex1a  44869  dvsid  44871  dvsef  44872  imassmpt  45801  elicores  46073  climresmpt  46197  dvcosre  46450  itgsinexplem1  46492  fourierdlem40  46685  fourierdlem57  46701  fourierdlem58  46702  fourierdlem62  46706  fourierdlem74  46718  fourierdlem75  46719  fourierdlem76  46720  fourierdlem80  46724  fourierdlem84  46728  fourierdlem85  46729  fourierdlem101  46745  fourierdlem102  46746  fourierdlem111  46755  fourierdlem114  46758  fouriersw  46769  fouriercn  46770  volicorescl  47091  fdmdifeqresdif  48928  tposresg  49463  tposrescnv  49464  rescofuf  49678  aacllem  50386