Theorem reseq1i 5928

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

Syntax hints:   = wceq 1541   ↾ cres 5621

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 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-in 3905  df-res 5631

This theorem is referenced by:  reseq12i  5930  resindm  5983  resmpt  5990  resmpt3  5991  resmptf  5992  elimampt  5996  opabresid  6003  rescnvcnv  6156  coires1  6217  fnunres2  6599  fresaunres1  6701  fcoi1  6702  fninfp  7114  fvsnun1  7122  fvsnun2  7123  resoprab  7470  resmpo  7472  elimampo  7489  elrnmpores  7490  ofmres  7922  f1stres  7951  f2ndres  7952  df1st2  8034  df2nd2  8035  fsplitfpar  8054  dftpos2  8179  frrlem12  8233  tfr2a  8320  tfr2b  8321  rdgseg  8347  frsucmpt2  8365  seqomlem2  8376  seqomlem3  8377  seqomlem4  8378  domss2  9056  dffi3  9322  axdc  10419  fpwwe2lem12  10540  seqval  13921  hashgval  14242  hashinf  14244  submefmnd  18805  pgrpsubgsymg  19323  gsumzunsnd  19870  ablfac1b  19986  zzngim  21491  pmatcollpw3lem  22699  txflf  23922  xmsxmet2  24375  msmet2  24376  tmsxpsmopn  24453  isngp2  24513  subgnm  24549  tngngp2  24568  cnfldms  24691  msdcn  24758  oprpiece1res1  24877  oprpiece1res2  24878  isncvsngp  25077  cncms  25283  cnfldcusp  25285  reust  25309  minveclem3a  25355  dvreslem  25838  dvres2lem  25839  dvmptresicc  25845  dvcmulf  25876  mdegfval  25995  psercn  26364  abelth  26379  efcvx  26387  efifo  26484  dfrelog  26502  dvrelog  26574  dvlog  26588  efopnlem2  26594  dvatan  26873  dchrisumlem1  27428  noetasuplem2  27674  noetasuplem3  27675  noetasuplem4  27676  noetainflem2  27678  wlknwwlksnbij  29868  df1stres  32689  df2ndres  32690  padct  32705  ressplusf  32951  ressnm  32952  gsummpt2d  33036  cycpmrn  33119  tocyccntz  33120  cycpmconjslem2  33131  qusima  33380  qqhcn  34025  cnrrext  34044  rrhre  34055  esumcvg  34120  dya2icoseg2  34312  eulerpartgbij  34406  satf0  35437  neibastop2  36426  mptsnunlem  37403  icorempo  37416  poimirlem3  37683  mbfposadd  37727  ftc1anclem3  37755  dvasin  37764  dvacos  37765  prdsbnd2  37855  repwsmet  37894  rrnequiv  37895  inres2  38302  xrnres  38469  xrnres2  38470  xrnres3  38471  diophin  42889  eldioph4b  42928  dnnumch1  43161  aomclem6  43176  radcnvrat  44431  lhe4.4ex1a  44446  dvsid  44448  dvsef  44449  imassmpt  45383  elicores  45657  climresmpt  45781  dvcosre  46034  itgsinexplem1  46076  fourierdlem40  46269  fourierdlem57  46285  fourierdlem58  46286  fourierdlem62  46290  fourierdlem74  46302  fourierdlem75  46303  fourierdlem76  46304  fourierdlem80  46308  fourierdlem84  46312  fourierdlem85  46313  fourierdlem101  46329  fourierdlem102  46330  fourierdlem111  46339  fourierdlem114  46342  fouriersw  46353  fouriercn  46354  volicorescl  46675  fdmdifeqresdif  48466  tposresg  49002  tposrescnv  49003  rescofuf  49218  aacllem  49926