Theorem reseq1i 5392

Description: Equality inference for restrictions. (Contributed by NM, 21-Oct-2014.)

Hypothesis

Ref	Expression
reseqi.1	|- A = B

Assertion

Ref	Expression
reseq1i	|- ( A |` C ) = ( B |` C )

Proof of Theorem reseq1i

Step	Hyp	Ref	Expression
1		reseqi.1	. 2 |- A = B
2		reseq1 5390	. 2 |- ( A = B -> ( A |` C ) = ( B |` C ) )
3	1, 2	ax-mp 5	1 |- ( A |` C ) = ( B |` C )

Syntax hints:   = wceq 1483   |` cres 5116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-res 5126

This theorem is referenced by:  reseq12i  5394  resindm  5444  resmpt  5449  resmpt3  5450  resmptf  5451  opabresid  5455  rescnvcnv  5597  coires1  5653  fresaunres1  6077  fcoi1  6078  fninfp  6440  fvsnun1  6448  fvsnun2  6449  resoprab  6756  resmpt2  6758  elrnmpt2res  6774  ofmres  7164  f1stres  7190  f2ndres  7191  df1st2  7263  df2nd2  7264  dftpos2  7369  wfrlem14  7428  tfr2a  7491  tfr2b  7492  rdgseg  7518  frsucmpt2  7535  seqomlem2  7546  seqomlem3  7547  seqomlem4  7548  domss2  8119  dffi3  8337  fpwwe2lem13  9464  seqval  12812  hashgval  13120  hashinf  13122  pgrpsubgsymg  17828  gsumzunsnd  18355  ablfac1b  18469  zzngim  19901  pmatcollpw3lem  20588  cnmptid  21464  txflf  21810  xmsxmet2  22264  msmet2  22265  tmsxpsmopn  22342  isngp2  22401  subgnm  22437  tngngp2  22456  cnfldms  22579  msdcn  22644  oprpiece1res1  22750  oprpiece1res2  22751  isncvsngp  22949  cncms  23151  cnfldcusp  23153  reust  23169  minveclem3a  23198  dvreslem  23673  dvres2lem  23674  dvcmulf  23708  mdegfval  23822  psercn  24180  abelth  24195  efcvx  24203  efifo  24293  dfrelog  24312  dvrelog  24383  dvlog  24397  efopnlem2  24403  dvatan  24662  dchrisumlem1  25178  elimampt  29438  df1stres  29481  df2ndres  29482  padct  29497  ressplusf  29650  ressnm  29651  gsummpt2d  29781  qqhcn  30035  cnrrext  30054  rrhre  30065  esumcvg  30148  dya2icoseg2  30340  eulerpartgbij  30434  trpred0  31736  noetalem2  31864  noetalem3  31865  neibastop2  32356  mptsnunlem  33185  icorempt2  33199  poimirlem3  33412  mbfposadd  33457  ftc1anclem3  33487  dvasin  33496  dvacos  33497  prdsbnd2  33594  repwsmet  33633  rrnequiv  33634  inres2  34007  diophin  37336  eldioph4b  37375  dnnumch1  37614  aomclem6  37629  radcnvrat  38513  lhe4.4ex1a  38528  dvsid  38530  dvsef  38531  imassmpt  39481  elicores  39760  climresmpt  39891  dvcosre  40126  dvmptresicc  40134  itgsinexplem1  40169  fourierdlem40  40364  fourierdlem57  40380  fourierdlem58  40381  fourierdlem62  40385  fourierdlem74  40397  fourierdlem75  40398  fourierdlem76  40399  fourierdlem80  40403  fourierdlem84  40407  fourierdlem85  40408  fourierdlem101  40424  fourierdlem102  40425  fourierdlem111  40434  fourierdlem114  40437  fouriersw  40448  fouriercn  40449  volicorescl  40767  fdmdifeqresdif  42120  aacllem  42547