Theorem reseq1i 5924

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

Syntax hints:   = wceq 1541   ↾ cres 5618

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-in 3909  df-res 5628

This theorem is referenced by:  reseq12i  5926  resindm  5979  resmpt  5986  resmpt3  5987  resmptf  5988  elimampt  5992  opabresid  5999  rescnvcnv  6151  coires1  6212  fnunres2  6594  fresaunres1  6696  fcoi1  6697  fninfp  7108  fvsnun1  7116  fvsnun2  7117  resoprab  7464  resmpo  7466  elimampo  7483  elrnmpores  7484  ofmres  7916  f1stres  7945  f2ndres  7946  df1st2  8028  df2nd2  8029  fsplitfpar  8048  dftpos2  8173  frrlem12  8227  tfr2a  8314  tfr2b  8315  rdgseg  8341  frsucmpt2  8359  seqomlem2  8370  seqomlem3  8371  seqomlem4  8372  domss2  9049  dffi3  9315  axdc  10409  fpwwe2lem12  10530  seqval  13916  hashgval  14237  hashinf  14239  submefmnd  18800  pgrpsubgsymg  19319  gsumzunsnd  19866  ablfac1b  19982  zzngim  21487  pmatcollpw3lem  22696  txflf  23919  xmsxmet2  24372  msmet2  24373  tmsxpsmopn  24450  isngp2  24510  subgnm  24546  tngngp2  24565  cnfldms  24688  msdcn  24755  oprpiece1res1  24874  oprpiece1res2  24875  isncvsngp  25074  cncms  25280  cnfldcusp  25282  reust  25306  minveclem3a  25352  dvreslem  25835  dvres2lem  25836  dvmptresicc  25842  dvcmulf  25873  mdegfval  25992  psercn  26361  abelth  26376  efcvx  26384  efifo  26481  dfrelog  26499  dvrelog  26571  dvlog  26585  efopnlem2  26591  dvatan  26870  dchrisumlem1  27425  noetasuplem2  27671  noetasuplem3  27672  noetasuplem4  27673  noetainflem2  27675  wlknwwlksnbij  29864  df1stres  32680  df2ndres  32681  padct  32696  ressplusf  32939  ressnm  32940  gsummpt2d  33024  cycpmrn  33107  tocyccntz  33108  cycpmconjslem2  33119  qusima  33368  qqhcn  33999  cnrrext  34018  rrhre  34029  esumcvg  34094  dya2icoseg2  34286  eulerpartgbij  34380  satf0  35404  neibastop2  36394  mptsnunlem  37371  icorempo  37384  poimirlem3  37662  mbfposadd  37706  ftc1anclem3  37734  dvasin  37743  dvacos  37744  prdsbnd2  37834  repwsmet  37873  rrnequiv  37874  inres2  38279  xrnres  38433  xrnres2  38434  xrnres3  38435  diophin  42804  eldioph4b  42843  dnnumch1  43076  aomclem6  43091  radcnvrat  44346  lhe4.4ex1a  44361  dvsid  44363  dvsef  44364  imassmpt  45298  elicores  45572  climresmpt  45696  dvcosre  45949  itgsinexplem1  45991  fourierdlem40  46184  fourierdlem57  46200  fourierdlem58  46201  fourierdlem62  46205  fourierdlem74  46217  fourierdlem75  46218  fourierdlem76  46219  fourierdlem80  46223  fourierdlem84  46227  fourierdlem85  46228  fourierdlem101  46244  fourierdlem102  46245  fourierdlem111  46254  fourierdlem114  46257  fouriersw  46268  fouriercn  46269  volicorescl  46590  fdmdifeqresdif  48372  tposresg  48908  tposrescnv  48909  rescofuf  49124  aacllem  49832