Theorem reseq2d 5094

Description: Equality deduction for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypothesis

Ref	Expression
reseqd.1	|- ( ph -> A = B )

Assertion

Ref	Expression
reseq2d	|- ( ph -> ( C |` A ) = ( C |` B ) )

Proof of Theorem reseq2d

Step	Hyp	Ref	Expression
1		reseqd.1	. 2 |- ( ph -> A = B )
2		reseq2 5089	. 2 |- ( A = B -> ( C |` A ) = ( C |` B ) )
3	1, 2	syl 17	1 |- ( ph -> ( C |` A ) = ( C |` B ) )

Syntax hints:   -> wi 4   = wceq 1405   |` cres 4825

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-v 3061  df-in 3421  df-opab 4454  df-xp 4829  df-res 4835

This theorem is referenced by:  reseq12d  5095  resima2  5127  resdmdfsn  5139  relresfld  5350  f1orescnv  5814  funcocnv2  5823  fococnv2  5824  fvn0ssdmfun  6000  fnressn  6063  fnsnsplit  6088  oprssov  6425  curry1  6876  curry2  6879  dftpos2  6975  wrecseq123  7014  wfr3g  7019  wfrlem1  7020  wfrlem4  7024  wfrlem14  7034  wfr2a  7038  dfrecs3  7076  tfrlem16  7096  tfr2ALT  7104  tfr3ALT  7105  sbthlem4  7668  mapunen  7724  hartogslem1  8001  axdc3lem2  8863  fseq1p1m1  11807  hashf1lem1  12553  relexp0g  13004  relexp0  13005  relexpsucnnr  13007  dfrtrcl2  13044  bpolylem  13993  setsval  14866  idfuval  15489  idfu2nd  15490  resf1st  15507  setcid  15689  catcisolem  15709  estrcid  15727  funcestrcsetclem5  15737  funcsetcestrclem5  15752  funcsetcestrclem7  15754  1stfval  15784  1stf2  15786  2ndfval  15787  2ndf2  15789  1stfcl  15790  2ndfcl  15791  curf2ndf  15840  hofcl  15852  isps  16156  cnvps  16166  isdir  16186  dirref  16189  tsrdir  16192  frmdval  16343  frmdplusg  16346  gsum2dlem2  17319  gsum2dOLD  17321  dprd2da  17411  dpjval  17425  ablfac1eulem  17443  ablfac1eu  17444  psrplusg  18354  opsrtoslem2  18469  mdetunilem3  19408  mdetunilem4  19409  mdetunilem9  19414  imacmp  20190  ptuncnv  20600  tgphaus  20907  tsmsresOLD  20937  tsmsres  20938  tsmsxplem1  20947  tsmsxplem2  20948  trust  21024  metreslem  21157  imasdsf1olem  21168  xmspropd  21268  mspropd  21269  imasf1oxms  21284  imasf1oms  21285  nmpropd2  21407  isngp2  21409  ngppropd  21443  tngngp2  21458  cmspropd  22080  mbfres2  22344  limciun  22590  dvmptres3  22651  dvmptres2  22657  dvmptntr  22666  dvlipcn  22687  dvlip2  22688  c1liplem1  22689  dvgt0lem1  22695  lhop1lem  22706  dvcnvrelem1  22710  dvcvx  22713  ftc2ditglem  22738  wilthlem2  23724  dchrval  23890  dchrelbas2  23893  ausisusgraedg  24773  1pthonlem1  25008  constr2pth  25020  eupath2lem3  25396  eupath2  25397  efghgrpOLD  25789  drngoi  25823  isdivrngo  25847  hhssablo  26593  hhssnvt  26595  hhsssh  26599  resf1o  28000  gsummpt2d  28223  qtophaus  28292  esumcvg  28533  eulerpartlemn  28826  sseqp1  28840  signsvtn0  29033  bnj1385  29218  bnj1326  29409  bnj1321  29410  bnj1442  29432  bnj1450  29433  bnj1463  29438  bnj1529  29453  cvmliftlem5  29586  cvmliftlem7  29588  cvmliftlem10  29591  cvmliftlem11  29592  cvmliftlem15  29595  cvmlift2lem11  29610  cvmlift2lem12  29611  ghomgrplem  29881  eldm3  29975  funsseq  29982  frr3g  30086  frrlem1  30087  frrlem4  30090  finixpnum  31410  sdclem2  31517  prdsbnd2  31573  dibffval  34160  hdmapffval  34849  hdmapfval  34850  eldiophb  35051  diophrw  35053  diophin  35067  dfrcl2  35653  fvmptiunrelexplb0da  35664  sblpnf  36038  fresin2  36823  cncfuni  37057  dvresntr  37081  dvbdfbdioolem1  37093  itgiccshift  37147  itgperiod  37148  dirkercncflem2  37254  fourierdlem46  37303  fourierdlem48  37305  fourierdlem49  37306  fourierdlem58  37315  fourierdlem72  37329  fourierdlem74  37331  fourierdlem75  37332  fourierdlem81  37338  fourierdlem88  37345  fourierdlem89  37346  fourierdlem90  37347  fourierdlem91  37348  fourierdlem92  37349  fourierdlem103  37360  fourierdlem104  37361  fourierdlem112  37369  fouriersw  37382  funcoressn  37580  usgra2pthspth  37980  idfusubc0  38182  idfusubc  38183  rngcval  38281  rnghmsubcsetclem1  38294  rngccat  38297  rngcid  38298  rngcidALTV  38310  rngcifuestrc  38316  funcrngcsetc  38317  funcrngcsetcALT  38318  ringcval  38327  rhmsubcsetclem1  38340  ringccat  38343  ringcid  38344  rhmsubcrngclem1  38346  rhmsubcrngc  38348  funcringcsetc  38354  funcringcsetcALTV2lem5  38359  ringcidALTV  38373  funcringcsetclem5ALTV  38382  rhmsubc  38409  rhmsubcALTVlem3  38426  aacllem  38860