Theorem reseq1i 5930

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 5928	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)

Syntax hints:   = wceq 1540   ↾ cres 5625

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-in 3912  df-res 5635

This theorem is referenced by:  reseq12i  5932  resindm  5985  resmpt  5992  resmpt3  5993  resmptf  5994  elimampt  5998  opabresid  6005  rescnvcnv  6157  coires1  6217  fnunres2  6599  fresaunres1  6701  fcoi1  6702  fninfp  7114  fvsnun1  7122  fvsnun2  7123  resoprab  7471  resmpo  7473  elimampo  7490  elrnmpores  7491  ofmres  7926  f1stres  7955  f2ndres  7956  df1st2  8038  df2nd2  8039  fsplitfpar  8058  dftpos2  8183  frrlem12  8237  tfr2a  8324  tfr2b  8325  rdgseg  8351  frsucmpt2  8369  seqomlem2  8380  seqomlem3  8381  seqomlem4  8382  domss2  9060  dffi3  9340  axdc  10434  fpwwe2lem12  10555  seqval  13937  hashgval  14258  hashinf  14260  submefmnd  18787  pgrpsubgsymg  19306  gsumzunsnd  19853  ablfac1b  19969  zzngim  21477  pmatcollpw3lem  22686  txflf  23909  xmsxmet2  24363  msmet2  24364  tmsxpsmopn  24441  isngp2  24501  subgnm  24537  tngngp2  24556  cnfldms  24679  msdcn  24746  oprpiece1res1  24865  oprpiece1res2  24866  isncvsngp  25065  cncms  25271  cnfldcusp  25273  reust  25297  minveclem3a  25343  dvreslem  25826  dvres2lem  25827  dvmptresicc  25833  dvcmulf  25864  mdegfval  25983  psercn  26352  abelth  26367  efcvx  26375  efifo  26472  dfrelog  26490  dvrelog  26562  dvlog  26576  efopnlem2  26582  dvatan  26861  dchrisumlem1  27416  noetasuplem2  27662  noetasuplem3  27663  noetasuplem4  27664  noetainflem2  27666  wlknwwlksnbij  29851  df1stres  32660  df2ndres  32661  padct  32676  ressplusf  32918  ressnm  32919  gsummpt2d  33015  cycpmrn  33098  tocyccntz  33099  cycpmconjslem2  33110  qusima  33355  qqhcn  33957  cnrrext  33976  rrhre  33987  esumcvg  34052  dya2icoseg2  34245  eulerpartgbij  34339  satf0  35344  neibastop2  36334  mptsnunlem  37311  icorempo  37324  poimirlem3  37602  mbfposadd  37646  ftc1anclem3  37674  dvasin  37683  dvacos  37684  prdsbnd2  37774  repwsmet  37813  rrnequiv  37814  inres2  38219  xrnres  38373  xrnres2  38374  xrnres3  38375  diophin  42745  eldioph4b  42784  dnnumch1  43017  aomclem6  43032  radcnvrat  44287  lhe4.4ex1a  44302  dvsid  44304  dvsef  44305  imassmpt  45240  elicores  45515  climresmpt  45641  dvcosre  45894  itgsinexplem1  45936  fourierdlem40  46129  fourierdlem57  46145  fourierdlem58  46146  fourierdlem62  46150  fourierdlem74  46162  fourierdlem75  46163  fourierdlem76  46164  fourierdlem80  46168  fourierdlem84  46172  fourierdlem85  46173  fourierdlem101  46189  fourierdlem102  46190  fourierdlem111  46199  fourierdlem114  46202  fouriersw  46213  fouriercn  46214  volicorescl  46535  fdmdifeqresdif  48327  tposresg  48863  tposrescnv  48864  rescofuf  49079  aacllem  49787