Theorem reseq2d 5122

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 5117	. 2 |- ( A = B -> ( C |` A ) = ( C |` B ) )
3	1, 2	syl 17	1 |- ( ph -> ( C |` A ) = ( C |` B ) )

Syntax hints:   -> wi 4   = wceq 1438   |` cres 4853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-v 3084  df-in 3444  df-opab 4481  df-xp 4857  df-res 4863

This theorem is referenced by:  reseq12d  5123  resima2  5155  resdmdfsn  5167  relresfld  5379  f1orescnv  5844  funcocnv2  5853  fococnv2  5854  fvn0ssdmfun  6026  fnressn  6089  fnsnsplit  6114  oprssov  6450  curry1  6897  curry2  6900  dftpos2  6996  wrecseq123  7035  wfr3g  7040  wfrlem1  7041  wfrlem4  7045  wfrlem14  7055  wfr2a  7059  dfrecs3  7097  tfrlem16  7117  tfr2ALT  7125  tfr3ALT  7126  sbthlem4  7689  mapunen  7745  hartogslem1  8061  axdc3lem2  8883  fseq1p1m1  11870  hashf1lem1  12617  relexp0g  13079  relexp0  13080  relexpsucnnr  13082  dfrtrcl2  13119  bpolylem  14094  setsval  15139  idfuval  15774  idfu2nd  15775  resf1st  15792  setcid  15974  catcisolem  15994  estrcid  16012  funcestrcsetclem5  16022  funcsetcestrclem5  16037  funcsetcestrclem7  16039  1stfval  16069  1stf2  16071  2ndfval  16072  2ndf2  16074  1stfcl  16075  2ndfcl  16076  curf2ndf  16125  hofcl  16137  isps  16441  cnvps  16451  isdir  16471  dirref  16474  tsrdir  16477  frmdval  16628  frmdplusg  16631  gsum2dlem2  17596  dprd2da  17668  dpjval  17682  ablfac1eulem  17698  ablfac1eu  17699  psrplusg  18598  opsrtoslem2  18701  mdetunilem3  19631  mdetunilem4  19632  mdetunilem9  19637  imacmp  20404  ptuncnv  20814  tgphaus  21123  tsmsres  21150  tsmsxplem1  21159  tsmsxplem2  21160  trust  21236  metreslem  21369  imasdsf1olem  21380  xmspropd  21480  mspropd  21481  imasf1oxms  21496  imasf1oms  21497  nmpropd2  21601  isngp2  21603  ngppropd  21637  tngngp2  21652  cmspropd  22309  mbfres2  22593  limciun  22841  dvmptres3  22902  dvmptres2  22908  dvmptntr  22917  dvlipcn  22938  dvlip2  22939  c1liplem1  22940  dvgt0lem1  22946  lhop1lem  22957  dvcnvrelem1  22961  dvcvx  22964  ftc2ditglem  22989  wilthlem2  23986  dchrval  24154  dchrelbas2  24157  ausisusgraedg  25075  1pthonlem1  25311  constr2pth  25323  eupath2lem3  25699  eupath2  25700  efghgrpOLD  26093  drngoi  26127  isdivrngo  26151  hhssablo  26906  hhssnvt  26908  hhsssh  26912  resf1o  28315  gsummpt2d  28545  qtophaus  28665  esumcvg  28909  eulerpartlemn  29216  sseqp1  29230  signsvtn0  29461  bnj1385  29646  bnj1326  29837  bnj1321  29838  bnj1442  29860  bnj1450  29861  bnj1463  29866  bnj1529  29881  cvmliftlem5  30014  cvmliftlem7  30016  cvmliftlem10  30019  cvmliftlem11  30020  cvmliftlem15  30023  cvmlift2lem11  30038  cvmlift2lem12  30039  ghomgrplem  30309  eldm3  30403  funsseq  30410  frr3g  30514  frrlem1  30515  frrlem4  30518  finixpnum  31888  poimirlem3  31901  poimirlem4  31902  poimirlem9  31907  sdclem2  32029  prdsbnd2  32085  dibffval  34671  hdmapffval  35360  hdmapfval  35361  eldiophb  35562  diophrw  35564  diophin  35578  dfrcl2  36170  fvmptiunrelexplb0da  36181  sblpnf  36560  fresin2  37329  cncfuni  37628  dvresntr  37652  dvbdfbdioolem1  37664  itgiccshift  37721  itgperiod  37722  dirkercncflem2  37830  fourierdlem46  37880  fourierdlem48  37882  fourierdlem49  37883  fourierdlem58  37892  fourierdlem72  37906  fourierdlem74  37908  fourierdlem75  37909  fourierdlem81  37915  fourierdlem88  37922  fourierdlem89  37923  fourierdlem90  37924  fourierdlem91  37925  fourierdlem92  37926  fourierdlem103  37937  fourierdlem104  37938  fourierdlem112  37946  fouriersw  37959  funcoressn  38385  usgra2pthspth  39007  idfusubc0  39207  idfusubc  39208  rngcval  39306  rnghmsubcsetclem1  39319  rngccat  39322  rngcid  39323  rngcidALTV  39335  rngcifuestrc  39341  funcrngcsetc  39342  funcrngcsetcALT  39343  ringcval  39352  rhmsubcsetclem1  39365  ringccat  39368  ringcid  39369  rhmsubcrngclem1  39371  rhmsubcrngc  39373  funcringcsetc  39379  funcringcsetcALTV2lem5  39384  ringcidALTV  39398  funcringcsetclem5ALTV  39407  rhmsubc  39434  rhmsubcALTVlem3  39451  aacllem  39884