Theorem reseq1i 5976

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

Syntax hints:   = wceq 1539   ↾ cres 5677

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-in 3954  df-res 5687

This theorem is referenced by:  reseq12i  5978  resindm  6029  resmpt  6036  resmpt3  6037  resmptf  6038  opabresid  6048  rescnvcnv  6202  coires1  6262  fnunres2  6661  fresaunres1  6763  fcoi1  6764  fninfp  7173  fvsnun1  7181  fvsnun2  7182  resoprab  7528  resmpo  7530  elrnmpores  7548  ofmres  7973  f1stres  8001  f2ndres  8002  df1st2  8086  df2nd2  8087  fsplitfpar  8106  dftpos2  8230  frrlem12  8284  wfrlem14OLD  8324  tfr2a  8397  tfr2b  8398  rdgseg  8424  frsucmpt2  8442  seqomlem2  8453  seqomlem3  8454  seqomlem4  8455  domss2  9138  dffi3  9428  fpwwe2lem12  10639  seqval  13981  hashgval  14297  hashinf  14299  submefmnd  18812  pgrpsubgsymg  19318  gsumzunsnd  19865  ablfac1b  19981  zzngim  21327  pmatcollpw3lem  22505  txflf  23730  xmsxmet2  24185  msmet2  24186  tmsxpsmopn  24266  isngp2  24326  subgnm  24362  tngngp2  24389  cnfldms  24512  msdcn  24577  oprpiece1res1  24696  oprpiece1res2  24697  isncvsngp  24897  cncms  25103  cnfldcusp  25105  reust  25129  minveclem3a  25175  dvreslem  25658  dvres2lem  25659  dvmptresicc  25665  dvcmulf  25696  mdegfval  25815  psercn  26174  abelth  26189  efcvx  26197  efifo  26292  dfrelog  26310  dvrelog  26381  dvlog  26395  efopnlem2  26401  dvatan  26676  dchrisumlem1  27228  noetasuplem2  27473  noetasuplem3  27474  noetasuplem4  27475  noetainflem2  27477  wlknwwlksnbij  29409  elimampt  32129  df1stres  32192  df2ndres  32193  padct  32211  ressplusf  32394  ressnm  32395  gsummpt2d  32471  cycpmrn  32572  tocyccntz  32573  cycpmconjslem2  32584  qusima  32793  qqhcn  33269  cnrrext  33288  rrhre  33299  esumcvg  33382  dya2icoseg2  33575  eulerpartgbij  33669  satf0  34661  neibastop2  35549  mptsnunlem  36522  icorempo  36535  poimirlem3  36794  mbfposadd  36838  ftc1anclem3  36866  dvasin  36875  dvacos  36876  prdsbnd2  36966  repwsmet  37005  rrnequiv  37006  inres2  37415  xrnres  37575  xrnres2  37576  xrnres3  37577  diophin  41812  eldioph4b  41851  dnnumch1  42088  aomclem6  42103  radcnvrat  43375  lhe4.4ex1a  43390  dvsid  43392  dvsef  43393  imassmpt  44265  elicores  44544  climresmpt  44673  dvcosre  44926  itgsinexplem1  44968  fourierdlem40  45161  fourierdlem57  45177  fourierdlem58  45178  fourierdlem62  45182  fourierdlem74  45194  fourierdlem75  45195  fourierdlem76  45196  fourierdlem80  45200  fourierdlem84  45204  fourierdlem85  45205  fourierdlem101  45221  fourierdlem102  45222  fourierdlem111  45231  fourierdlem114  45234  fouriersw  45245  fouriercn  45246  volicorescl  45567  fdmdifeqresdif  47105  aacllem  47935