Theorem reseq1i 5101

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

Syntax hints:   = wceq 1369   |` cres 4837

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-in 3330  df-res 4847

This theorem is referenced by:  reseq12i  5103  resindm  5146  resmpt  5151  resmpt3  5152  opabresid  5154  rescnvcnv  5296  coires1  5350  fresaunres1  5579  fcoi1  5580  fninfp  5900  fvsnun1  5908  fvsnun2  5909  resoprab  6181  resmpt2  6183  elrnmpt2res  6199  ofmres  6568  f1stres  6593  f2ndres  6594  df1st2  6654  df2nd2  6655  dftpos2  6757  tfr2a  6846  tfr2b  6847  rdgseg  6870  frsucmpt2  6887  seqomlem2  6898  seqomlem3  6899  seqomlem4  6900  domss2  7462  dffi3  7673  fpwwe2lem13  8801  seqval  11809  hashgval  12098  hashinf  12100  pgrpsubgsymg  15904  gsumzunsnd  16441  ablfac1b  16561  zzngim  17965  cnmptid  19214  txflf  19559  xmsxmet2  20014  msmet2  20015  tmsxpsmopn  20092  isngp2  20169  subgnm  20199  tngngp2  20218  cnfldms  20335  msdcn  20398  oprpiece1res1  20503  oprpiece1res2  20504  cncms  20847  cnfldcusp  20849  reust  20865  minveclem3a  20894  dvreslem  21364  dvres2lem  21365  dvcmulf  21399  mdegfval  21511  psercn  21871  abelth  21886  efcvx  21894  efifo  21983  dfrelog  21997  dvrelog  22062  dvlog  22076  efopnlem2  22082  dvatan  22310  dchrisumlem1  22718  constr3pthlem1  23509  resmptf  25942  df1stres  25967  df2ndres  25968  ressplusf  26079  ressnm  26080  qqhcn  26389  cnrrext  26408  rrhre  26416  esumcvg  26504  dya2icoseg2  26662  eulerpartgbij  26724  trpred0  27669  wfrlem14  27706  mbfposadd  28410  ftc1anclem3  28440  dvasin  28451  dvacos  28452  neibastop2  28553  prdsbnd2  28665  repwsmet  28704  rrnequiv  28705  diophin  29082  eldioph4b  29121  dnnumch1  29368  aomclem6  29383  lhe4.4ex1a  29574  dvsid  29576  dvsef  29577  dvcosre  29759  itgsinexplem1  29765  fdmdifeqresdif  30702