Theorem reseq1i 5976

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

Syntax hints:   = wceq 1570   ↾ cres 5665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-in 3913  df-res 5675

This theorem is referenced by:  reseq12i  5978  resindmOLD  6032  resmpt  6041  resmpt3  6042  resmptf  6043  elimampt  6047  opabresid  6054  rescnvcnv  6207  coires1  6268  fnunres2  6650  fresaunres1  6753  fcoi1  6754  fninfp  7174  fvsnun1  7182  fvsnun2  7183  resoprab  7530  resmpo  7532  elimampo  7549  elrnmpores  7550  ofmres  7982  f1stres  8011  f2ndres  8012  df1st2  8094  df2nd2  8095  fsplitfpar  8114  dftpos2  8240  frrlem12  8295  tfr2a  8383  tfr2b  8384  rdgseg  8410  frsucmpt2  8428  seqomlem2  8439  seqomlem3  8440  seqomlem4  8441  domss2  9125  dffi3  9392  axdc  10506  fpwwe2lem12  10628  seqval  14050  hashgval  14371  hashinf  14373  submefmnd  18955  pgrpsubgsymg  19480  gsumzunsnd  20027  ablfac1b  20143  zzngim  21683  pmatcollpw3lem  22921  txflf  24144  xmsxmet2  24597  msmet2  24598  tmsxpsmopn  24675  isngp2  24735  subgnm  24771  tngngp2  24790  cnfldms  24913  msdcn  24980  oprpiece1res1  25091  oprpiece1res2  25092  isncvsngp  25289  cncms  25495  cnfldcusp  25497  reust  25521  minveclem3a  25567  dvreslem  26049  dvres2lem  26050  dvmptresicc  26056  dvcmulf  26085  mdegfval  26200  psercn  26567  abelth  26582  efcvx  26590  efifo  26690  dfrelog  26708  dvrelog  26780  dvlog  26794  efopnlem2  26800  dvatan  27078  dchrisumlem1  27631  noetasuplem2  27876  noetasuplem3  27877  noetasuplem4  27878  noetainflem2  27880  wlknwwlksnbij  30215  df1stres  33027  df2ndres  33028  padct  33041  ressplusf  33261  ressnm  33262  gsummpt2d  33347  cycpmrn  33441  tocyccntz  33442  cycpmconjslem2  33453  qusima  33695  qqhcn  34359  cnrrext  34378  rrhre  34389  esumcvg  34454  dya2icoseg2  34646  eulerpartgbij  34740  satf0  35842  neibastop2  36850  mptsnunlem  37962  icorempo  37975  poimirlem3  38252  mbfposadd  38296  ftc1anclem3  38324  dvasin  38333  dvacos  38334  prdsbnd2  38424  repwsmet  38463  rrnequiv  38464  inres2  38874  xrnres  39052  xrnres2  39053  xrnres3  39054  diophin  43483  eldioph4b  43518  dnnumch1  43751  aomclem6  43766  radcnvrat  45004  lhe4.4ex1a  45019  dvsid  45021  dvsef  45022  imassmpt  45957  elicores  46229  climresmpt  46353  dvcosre  46606  itgsinexplem1  46648  fourierdlem40  46841  fourierdlem57  46857  fourierdlem58  46858  fourierdlem62  46862  fourierdlem74  46874  fourierdlem75  46875  fourierdlem76  46876  fourierdlem80  46880  fourierdlem84  46884  fourierdlem85  46885  fourierdlem101  46901  fourierdlem102  46902  fourierdlem111  46911  fourierdlem114  46914  fouriersw  46925  fouriercn  46926  volicorescl  47247  fdmdifeqresdif  49099  tposresg  49633  tposrescnv  49634  rescofuf  49848  aacllem  50578