Theorem reseq1i 5313

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

Syntax hints:   = wceq 1475   ↾ cres 5040

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-res 5050

This theorem is referenced by:  reseq12i  5315  resindm  5364  resmpt  5369  resmpt3  5370  opabresid  5374  rescnvcnv  5515  coires1  5570  fresaunres1  5990  fcoi1  5991  fninfp  6345  fvsnun1  6353  fvsnun2  6354  resoprab  6654  resmpt2  6656  elrnmpt2res  6672  ofmres  7055  f1stres  7081  f2ndres  7082  df1st2  7150  df2nd2  7151  dftpos2  7256  wfrlem14  7315  tfr2a  7378  tfr2b  7379  rdgseg  7405  frsucmpt2  7422  seqomlem2  7433  seqomlem3  7434  seqomlem4  7435  domss2  8004  dffi3  8220  fpwwe2lem13  9343  seqval  12674  hashgval  12982  hashinf  12984  pgrpsubgsymg  17651  gsumzunsnd  18178  ablfac1b  18292  zzngim  19720  pmatcollpw3lem  20407  cnmptid  21274  txflf  21620  xmsxmet2  22074  msmet2  22075  tmsxpsmopn  22152  isngp2  22211  subgnm  22247  tngngp2  22266  cnfldms  22389  msdcn  22452  oprpiece1res1  22558  oprpiece1res2  22559  isncvsngp  22757  cncms  22959  cnfldcusp  22961  reust  22977  minveclem3a  23006  dvreslem  23479  dvres2lem  23480  dvcmulf  23514  mdegfval  23626  psercn  23984  abelth  23999  efcvx  24007  efifo  24097  dfrelog  24116  dvrelog  24183  dvlog  24197  efopnlem2  24203  dvatan  24462  dchrisumlem1  24978  constr3pthlem1  26183  resmptf  28838  df1stres  28864  df2ndres  28865  padct  28885  ressplusf  28981  ressnm  28982  gsummpt2d  29112  qqhcn  29363  cnrrext  29382  rrhre  29393  esumcvg  29475  dya2icoseg2  29667  eulerpartgbij  29761  trpred0  30980  neibastop2  31526  mptsnunlem  32361  icorempt2  32375  poimirlem3  32582  mbfposadd  32627  ftc1anclem3  32657  dvasin  32666  dvacos  32667  prdsbnd2  32764  repwsmet  32803  rrnequiv  32804  diophin  36354  eldioph4b  36393  dnnumch1  36632  aomclem6  36647  radcnvrat  37535  lhe4.4ex1a  37550  dvsid  37552  dvsef  37553  elicores  38607  climresmpt  38726  dvcosre  38799  dvmptresicc  38809  itgsinexplem1  38845  fourierdlem40  39040  fourierdlem57  39056  fourierdlem58  39057  fourierdlem62  39061  fourierdlem74  39073  fourierdlem75  39074  fourierdlem76  39075  fourierdlem80  39079  fourierdlem84  39083  fourierdlem85  39084  fourierdlem101  39100  fourierdlem102  39101  fourierdlem111  39110  fourierdlem114  39113  fouriersw  39124  fouriercn  39125  volicorescl  39443  fdmdifeqresdif  41913  aacllem  42356