Theorem reseq1i 5260

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 5258	. 2 |- ( A = B -> ( A |` C ) = ( B |` C ) )
3	1, 2	ax-mp 5	1 |- ( A |` C ) = ( B |` C )

Syntax hints:   = wceq 1374   |` cres 4994

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-v 3108  df-in 3476  df-res 5004

This theorem is referenced by:  reseq12i  5262  resindm  5309  resmpt  5314  resmpt3  5315  opabresid  5318  rescnvcnv  5461  coires1  5516  fresaunres1  5749  fcoi1  5750  fninfp  6079  fvsnun1  6087  fvsnun2  6088  resoprab  6373  resmpt2  6375  elrnmpt2res  6391  ofmres  6770  f1stres  6796  f2ndres  6797  df1st2  6859  df2nd2  6860  dftpos2  6962  tfr2a  7054  tfr2b  7055  rdgseg  7078  frsucmpt2  7095  seqomlem2  7106  seqomlem3  7107  seqomlem4  7108  domss2  7666  dffi3  7880  fpwwe2lem13  9009  seqval  12074  hashgval  12363  hashinf  12365  pgrpsubgsymg  16221  gsumzunsnd  16766  ablfac1b  16904  zzngim  18351  pmatcollpw3lem  19044  cnmptid  19890  txflf  20235  xmsxmet2  20690  msmet2  20691  tmsxpsmopn  20768  isngp2  20845  subgnm  20875  tngngp2  20894  cnfldms  21011  msdcn  21074  oprpiece1res1  21179  oprpiece1res2  21180  cncms  21523  cnfldcusp  21525  reust  21541  minveclem3a  21570  dvreslem  22041  dvres2lem  22042  dvcmulf  22076  mdegfval  22188  psercn  22548  abelth  22563  efcvx  22571  efifo  22660  dfrelog  22674  dvrelog  22739  dvlog  22753  efopnlem2  22759  dvatan  22987  dchrisumlem1  23395  constr3pthlem1  24317  resmptf  27019  df1stres  27044  df2ndres  27045  ressplusf  27150  ressnm  27151  qqhcn  27458  cnrrext  27477  rrhre  27485  esumcvg  27582  dya2icoseg2  27739  eulerpartgbij  27801  trpred0  28746  wfrlem14  28783  mbfposadd  29490  ftc1anclem3  29520  dvasin  29531  dvacos  29532  neibastop2  29633  prdsbnd2  29745  repwsmet  29784  rrnequiv  29785  diophin  30161  eldioph4b  30200  dnnumch1  30447  aomclem6  30462  lhe4.4ex1a  30653  dvsid  30655  dvsef  30656  dvcosre  31058  dvmptresicc  31068  itgsinexplem1  31090  fourierdlem40  31266  fourierdlem57  31283  fourierdlem58  31284  fourierdlem62  31288  fourierdlem74  31300  fourierdlem75  31301  fourierdlem76  31302  fourierdlem80  31306  fourierdlem84  31310  fourierdlem85  31311  fourierdlem101  31327  fourierdlem102  31328  fourierdlem111  31337  fourierdlem114  31340  fouriersw  31351  fouriercn  31352  fdmdifeqresdif  31870