Theorem reseq1i 5876

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

Syntax hints:   = wceq 1539   ↾ cres 5582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-in 3890  df-res 5592

This theorem is referenced by:  reseq12i  5878  resindm  5929  resmpt  5934  resmpt3  5935  resmptf  5936  opabresid  5946  opabresidOLD  5948  rescnvcnv  6096  coires1  6157  fresaunres1  6631  fcoi1  6632  fninfp  7028  fvsnun1  7036  fvsnun2  7037  resoprab  7370  resmpo  7372  elrnmpores  7389  ofmres  7800  f1stres  7828  f2ndres  7829  df1st2  7909  df2nd2  7910  fsplitfpar  7930  dftpos2  8030  frrlem12  8084  wfrlem14OLD  8124  tfr2a  8197  tfr2b  8198  rdgseg  8224  frsucmpt2  8241  seqomlem2  8252  seqomlem3  8253  seqomlem4  8254  domss2  8872  dffi3  9120  trpred0  9410  fpwwe2lem12  10329  seqval  13660  hashgval  13975  hashinf  13977  submefmnd  18449  pgrpsubgsymg  18932  gsumzunsnd  19472  ablfac1b  19588  zzngim  20672  pmatcollpw3lem  21840  txflf  23065  xmsxmet2  23520  msmet2  23521  tmsxpsmopn  23599  isngp2  23659  subgnm  23695  tngngp2  23722  cnfldms  23845  msdcn  23910  oprpiece1res1  24020  oprpiece1res2  24021  isncvsngp  24218  cncms  24424  cnfldcusp  24426  reust  24450  minveclem3a  24496  dvreslem  24978  dvres2lem  24979  dvmptresicc  24985  dvcmulf  25014  mdegfval  25132  psercn  25490  abelth  25505  efcvx  25513  efifo  25608  dfrelog  25626  dvrelog  25697  dvlog  25711  efopnlem2  25717  dvatan  25990  dchrisumlem1  26542  wlknwwlksnbij  28154  elimampt  30874  fnunres2  30917  df1stres  30938  df2ndres  30939  padct  30956  ressplusf  31137  ressnm  31138  gsummpt2d  31211  cycpmrn  31312  tocyccntz  31313  cycpmconjslem2  31324  qusima  31496  qqhcn  31841  cnrrext  31860  rrhre  31871  esumcvg  31954  dya2icoseg2  32145  eulerpartgbij  32239  satf0  33234  noetasuplem2  33864  noetasuplem3  33865  noetasuplem4  33866  noetainflem2  33868  neibastop2  34477  mptsnunlem  35436  icorempo  35449  poimirlem3  35707  mbfposadd  35751  ftc1anclem3  35779  dvasin  35788  dvacos  35789  prdsbnd2  35880  repwsmet  35919  rrnequiv  35920  inres2  36311  xrnres  36455  xrnres2  36456  xrnres3  36457  diophin  40510  eldioph4b  40549  dnnumch1  40785  aomclem6  40800  radcnvrat  41821  lhe4.4ex1a  41836  dvsid  41838  dvsef  41839  imassmpt  42699  elicores  42961  climresmpt  43090  dvcosre  43343  itgsinexplem1  43385  fourierdlem40  43578  fourierdlem57  43594  fourierdlem58  43595  fourierdlem62  43599  fourierdlem74  43611  fourierdlem75  43612  fourierdlem76  43613  fourierdlem80  43617  fourierdlem84  43621  fourierdlem85  43622  fourierdlem101  43638  fourierdlem102  43639  fourierdlem111  43648  fourierdlem114  43651  fouriersw  43662  fouriercn  43663  volicorescl  43981  fdmdifeqresdif  45565  aacllem  46391