Theorem reseq1i 5093

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

Syntax hints:   = wceq 1362   |` cres 4829

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-in 3323  df-res 4839

This theorem is referenced by:  reseq12i  5095  resindm  5139  resmpt  5144  resmpt3  5145  opabresid  5147  rescnvcnv  5289  coires1  5343  fresaunres1  5572  fcoi1  5573  fninfp  5892  fvsnun1  5900  fvsnun2  5901  resoprab  6175  resmpt2  6177  elrnmpt2res  6193  ofmres  6562  f1stres  6587  f2ndres  6588  df1st2  6648  df2nd2  6649  dftpos2  6751  tfr2a  6840  tfr2b  6841  rdgseg  6864  frsucmpt2  6881  seqomlem2  6892  seqomlem3  6893  seqomlem4  6894  domss2  7458  dffi3  7669  fpwwe2lem13  8797  seqval  11801  hashgval  12090  hashinf  12092  pgrpsubgsymg  15893  ablfac1b  16545  zzngim  17827  cnmptid  19076  txflf  19421  xmsxmet2  19876  msmet2  19877  tmsxpsmopn  19954  isngp2  20031  subgnm  20061  tngngp2  20080  cnfldms  20197  msdcn  20260  oprpiece1res1  20365  oprpiece1res2  20366  cncms  20709  cnfldcusp  20711  reust  20727  minveclem3a  20756  dvreslem  21226  dvres2lem  21227  dvcmulf  21261  mdegfval  21416  psercn  21776  abelth  21791  efcvx  21799  efifo  21888  dfrelog  21902  dvrelog  21967  dvlog  21981  efopnlem2  21987  dvatan  22215  dchrisumlem1  22623  constr3pthlem1  23364  resmptf  25798  df1stres  25823  df2ndres  25824  ressplusf  25934  ressnm  25935  qqhcn  26274  cnrrext  26293  rrhre  26301  esumcvg  26389  dya2icoseg2  26547  eulerpartgbij  26603  trpred0  27547  wfrlem14  27584  mbfposadd  28283  ftc1anclem3  28313  dvasin  28324  dvacos  28325  neibastop2  28426  prdsbnd2  28538  repwsmet  28577  rrnequiv  28578  diophin  28956  eldioph4b  28995  dnnumch1  29242  aomclem6  29257  lhe4.4ex1a  29448  dvsid  29450  dvsef  29451  dvcosre  29634  itgsinexplem1  29640  fdmdifeqresdif  30576