Theorem reseq1i 5975

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

Syntax hints:   = wceq 1567   ↾ cres 5664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-in 3920  df-res 5674

This theorem is referenced by:  reseq12i  5977  resindmOLD  6031  resmpt  6040  resmpt3  6041  resmptf  6042  elimampt  6046  opabresid  6053  rescnvcnv  6206  coires1  6267  fnunres2  6649  fresaunres1  6752  fcoi1  6753  fninfp  7173  fvsnun1  7181  fvsnun2  7182  resoprab  7529  resmpo  7531  elimampo  7548  elrnmpores  7549  ofmres  7981  f1stres  8010  f2ndres  8011  df1st2  8093  df2nd2  8094  fsplitfpar  8113  dftpos2  8239  frrlem12  8294  tfr2a  8382  tfr2b  8383  rdgseg  8409  frsucmpt2  8427  seqomlem2  8438  seqomlem3  8439  seqomlem4  8440  domss2  9124  dffi3  9391  axdc  10505  fpwwe2lem12  10627  seqval  14048  hashgval  14369  hashinf  14371  submefmnd  18954  pgrpsubgsymg  19479  gsumzunsnd  20026  ablfac1b  20142  zzngim  21671  pmatcollpw3lem  22909  txflf  24132  xmsxmet2  24585  msmet2  24586  tmsxpsmopn  24663  isngp2  24723  subgnm  24759  tngngp2  24778  cnfldms  24901  msdcn  24968  oprpiece1res1  25079  oprpiece1res2  25080  isncvsngp  25277  cncms  25483  cnfldcusp  25485  reust  25509  minveclem3a  25555  dvreslem  26037  dvres2lem  26038  dvmptresicc  26044  dvcmulf  26073  mdegfval  26188  psercn  26555  abelth  26570  efcvx  26578  efifo  26678  dfrelog  26696  dvrelog  26768  dvlog  26782  efopnlem2  26788  dvatan  27066  dchrisumlem1  27619  noetasuplem2  27864  noetasuplem3  27865  noetasuplem4  27866  noetainflem2  27868  wlknwwlksnbij  30178  df1stres  32990  df2ndres  32991  padct  33004  ressplusf  33224  ressnm  33225  gsummpt2d  33310  cycpmrn  33404  tocyccntz  33405  cycpmconjslem2  33416  qusima  33661  qqhcn  34326  cnrrext  34345  rrhre  34356  esumcvg  34421  dya2icoseg2  34613  eulerpartgbij  34707  satf0  35797  neibastop2  36795  mptsnunlem  37906  icorempo  37919  poimirlem3  38196  mbfposadd  38240  ftc1anclem3  38268  dvasin  38277  dvacos  38278  prdsbnd2  38368  repwsmet  38407  rrnequiv  38408  inres2  38820  xrnres  38998  xrnres2  38999  xrnres3  39000  diophin  43429  eldioph4b  43464  dnnumch1  43697  aomclem6  43712  radcnvrat  44950  lhe4.4ex1a  44965  dvsid  44967  dvsef  44968  imassmpt  45903  elicores  46175  climresmpt  46299  dvcosre  46552  itgsinexplem1  46594  fourierdlem40  46787  fourierdlem57  46803  fourierdlem58  46804  fourierdlem62  46808  fourierdlem74  46820  fourierdlem75  46821  fourierdlem76  46822  fourierdlem80  46826  fourierdlem84  46830  fourierdlem85  46831  fourierdlem101  46847  fourierdlem102  46848  fourierdlem111  46857  fourierdlem114  46860  fouriersw  46871  fouriercn  46872  volicorescl  47193  fdmdifeqresdif  49041  tposresg  49575  tposrescnv  49576  rescofuf  49790  aacllem  50509