Theorem reseq1i 5934

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

Syntax hints:   = wceq 1541   ↾ cres 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-in 3908  df-res 5636

This theorem is referenced by:  reseq12i  5936  resindm  5989  resmpt  5996  resmpt3  5997  resmptf  5998  elimampt  6002  opabresid  6009  rescnvcnv  6162  coires1  6223  fnunres2  6605  fresaunres1  6707  fcoi1  6708  fninfp  7120  fvsnun1  7128  fvsnun2  7129  resoprab  7476  resmpo  7478  elimampo  7495  elrnmpores  7496  ofmres  7928  f1stres  7957  f2ndres  7958  df1st2  8040  df2nd2  8041  fsplitfpar  8060  dftpos2  8185  frrlem12  8239  tfr2a  8326  tfr2b  8327  rdgseg  8353  frsucmpt2  8371  seqomlem2  8382  seqomlem3  8383  seqomlem4  8384  domss2  9064  dffi3  9334  axdc  10431  fpwwe2lem12  10553  seqval  13935  hashgval  14256  hashinf  14258  submefmnd  18820  pgrpsubgsymg  19338  gsumzunsnd  19885  ablfac1b  20001  zzngim  21507  pmatcollpw3lem  22727  txflf  23950  xmsxmet2  24403  msmet2  24404  tmsxpsmopn  24481  isngp2  24541  subgnm  24577  tngngp2  24596  cnfldms  24719  msdcn  24786  oprpiece1res1  24905  oprpiece1res2  24906  isncvsngp  25105  cncms  25311  cnfldcusp  25313  reust  25337  minveclem3a  25383  dvreslem  25866  dvres2lem  25867  dvmptresicc  25873  dvcmulf  25904  mdegfval  26023  psercn  26392  abelth  26407  efcvx  26415  efifo  26512  dfrelog  26530  dvrelog  26602  dvlog  26616  efopnlem2  26622  dvatan  26901  dchrisumlem1  27456  noetasuplem2  27702  noetasuplem3  27703  noetasuplem4  27704  noetainflem2  27706  wlknwwlksnbij  29961  df1stres  32783  df2ndres  32784  padct  32797  ressplusf  33045  ressnm  33046  gsummpt2d  33132  cycpmrn  33225  tocyccntz  33226  cycpmconjslem2  33237  qusima  33489  qqhcn  34148  cnrrext  34167  rrhre  34178  esumcvg  34243  dya2icoseg2  34435  eulerpartgbij  34529  satf0  35566  neibastop2  36555  mptsnunlem  37539  icorempo  37552  poimirlem3  37820  mbfposadd  37864  ftc1anclem3  37892  dvasin  37901  dvacos  37902  prdsbnd2  37992  repwsmet  38031  rrnequiv  38032  inres2  38439  xrnres  38606  xrnres2  38607  xrnres3  38608  diophin  43010  eldioph4b  43049  dnnumch1  43282  aomclem6  43297  radcnvrat  44551  lhe4.4ex1a  44566  dvsid  44568  dvsef  44569  imassmpt  45502  elicores  45775  climresmpt  45899  dvcosre  46152  itgsinexplem1  46194  fourierdlem40  46387  fourierdlem57  46403  fourierdlem58  46404  fourierdlem62  46408  fourierdlem74  46420  fourierdlem75  46421  fourierdlem76  46422  fourierdlem80  46426  fourierdlem84  46430  fourierdlem85  46431  fourierdlem101  46447  fourierdlem102  46448  fourierdlem111  46457  fourierdlem114  46460  fouriersw  46471  fouriercn  46472  volicorescl  46793  fdmdifeqresdif  48584  tposresg  49119  tposrescnv  49120  rescofuf  49334  aacllem  50042