Theorem reseq1i 5977

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

This proof depends on syntax axioms:   = wceq 1570   ↾ cres 5657

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-in 4094  df-res 5667

This theorem is used by:  reseq12i  5979  resindmOLD  6032  resmpt  6041  resmpt3  6042  resmptf  6043  elimampt  6047  opabresid  6054  rescnvcnv  6218  coires1  6282  fnunres2  6674  fresaunres1  6777  fcoi1  6778  fninfp  7202  fvsnun1  7210  fvsnun2  7211  resoprab  7561  resmpo  7563  elimampo  7581  elrnmpores  7582  ofmres  8020  f1stres  8049  f2ndres  8050  df1st2  8136  df2nd2  8137  fsplitfpar  8156  dftpos2  8288  frrlem12  8343  tfr2a  8431  tfr2b  8432  rdgseg  8458  frsucmpt2  8476  seqomlem2  8489  seqomlem3  8490  seqomlem4  8491  domss2  9183  dffi3  9450  axdc  10626  fpwwe2lem12  10754  seqval  14182  hashgval  14504  hashinf  14506  submefmnd  19120  pgrpsubgsymg  19653  gsumzunsnd  20200  ablfac1b  20316  zzngim  21888  pmatcollpw3lem  23131  txflf  24355  xmsxmet2  24808  msmet2  24809  tmsxpsmopn  24886  isngp2  24946  subgnm  24982  tngngp2  25001  cnfldms  25124  msdcn  25191  oprpiece1res1  25302  oprpiece1res2  25303  isncvsngp  25500  cncms  25706  cnfldcusp  25708  reust  25732  minveclem3a  25778  dvreslem  26259  dvres2lem  26260  dvmptresicc  26266  dvcmulf  26295  mdegfval  26410  psercn  26783  abelth  26798  efcvx  26806  efifo  26905  dfrelog  26923  dvrelog  26995  dvlog  27009  efopnlem2  27015  dvatan  27293  dchrisumlem1  27846  noetasuplem2  28121  noetasuplem3  28122  noetasuplem4  28123  noetainflem2  28125  wlknwwlksnbij  30507  df1stres  33368  df2ndres  33369  padct  33381  ressplusf  33594  ressnm  33595  gsummpt2d  33680  cycpmrn  33774  tocyccntz  33775  cycpmconjslem2  33786  qusima  34029  qqhcn  34693  cnrrext  34712  rrhre  34723  esumcvg  34788  dya2icoseg2  34980  eulerpartgbij  35074  srepdflem1  36085  satf0  36304  neibastop2  37327  mptsnunlem  38453  icorempo  38466  poimirlem3  38733  mbfposadd  38777  ftc1anclem3  38805  dvasin  38814  dvacos  38815  prdsbnd2  38921  repwsmet  38960  rrnequiv  38961  inres2  39371  xrnres  39549  xrnres2  39550  xrnres3  39551  diophin  43976  eldioph4b  44011  dnnumch1  44244  aomclem6  44254  radcnvrat  45490  lhe4.4ex1a  45505  dvsid  45507  dvsef  45508  imassmpt  46479  elicores  46750  climresmpt  46874  dvcosre  47127  itgsinexplem1  47169  fourierdlem40  47362  fourierdlem57  47378  fourierdlem58  47379  fourierdlem62  47383  fourierdlem74  47395  fourierdlem75  47396  fourierdlem76  47397  fourierdlem80  47401  fourierdlem84  47405  fourierdlem85  47406  fourierdlem101  47422  fourierdlem102  47423  fourierdlem111  47432  fourierdlem114  47435  fouriersw  47446  fouriercn  47447  volicorescl  47768  fdmdifeqresdif  49659  tposresg  50196  tposrescnv  50197  rescofuf  50413  aacllem  51219