Theorem reseq2d 5123

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

Syntax hints:   -> wi 4   = wceq 1454   |` cres 4854

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-v 3058  df-in 3422  df-opab 4475  df-xp 4858  df-res 4864

This theorem is referenced by:  reseq12d  5124  resima2  5156  resdmdfsn  5168  relresfld  5380  f1orescnv  5851  funcocnv2  5860  fococnv2  5861  fvn0ssdmfun  6035  fnressn  6099  fnsnsplit  6124  oprssov  6464  curry1  6914  curry2  6917  dftpos2  7015  wrecseq123  7054  wfr3g  7059  wfrlem1  7060  wfrlem4  7064  wfrlem14  7074  wfr2a  7078  dfrecs3  7116  tfrlem16  7136  tfr2ALT  7144  tfr3ALT  7145  sbthlem4  7710  mapunen  7766  hartogslem1  8082  axdc3lem2  8906  fseq1p1m1  11896  hashf1lem1  12650  relexp0g  13133  relexp0  13134  relexpsucnnr  13136  dfrtrcl2  13173  bpolylem  14149  setsval  15194  idfuval  15829  idfu2nd  15830  resf1st  15847  setcid  16029  catcisolem  16049  estrcid  16067  funcestrcsetclem5  16077  funcsetcestrclem5  16092  funcsetcestrclem7  16094  1stfval  16124  1stf2  16126  2ndfval  16127  2ndf2  16129  1stfcl  16130  2ndfcl  16131  curf2ndf  16180  hofcl  16192  isps  16496  cnvps  16506  isdir  16526  dirref  16529  tsrdir  16532  frmdval  16683  frmdplusg  16686  gsum2dlem2  17651  dprd2da  17723  dpjval  17737  ablfac1eulem  17753  ablfac1eu  17754  psrplusg  18653  opsrtoslem2  18756  mdetunilem3  19687  mdetunilem4  19688  mdetunilem9  19693  imacmp  20460  ptuncnv  20870  tgphaus  21179  tsmsres  21206  tsmsxplem1  21215  tsmsxplem2  21216  trust  21292  metreslem  21425  imasdsf1olem  21436  xmspropd  21536  mspropd  21537  imasf1oxms  21552  imasf1oms  21553  nmpropd2  21657  isngp2  21659  ngppropd  21693  tngngp2  21708  cmspropd  22365  mbfres2  22649  limciun  22897  dvmptres3  22958  dvmptres2  22964  dvmptntr  22973  dvlipcn  22994  dvlip2  22995  c1liplem1  22996  dvgt0lem1  23002  lhop1lem  23013  dvcnvrelem1  23017  dvcvx  23020  ftc2ditglem  23045  wilthlem2  24042  dchrval  24210  dchrelbas2  24213  ausisusgraedg  25131  1pthonlem1  25367  constr2pth  25379  eupath2lem3  25755  eupath2  25756  efghgrpOLD  26149  drngoi  26183  isdivrngo  26207  hhssablo  26962  hhssnvt  26964  hhsssh  26968  resf1o  28363  gsummpt2d  28592  qtophaus  28711  esumcvg  28955  eulerpartlemn  29262  sseqp1  29276  signsvtn0  29507  bnj1385  29692  bnj1326  29883  bnj1321  29884  bnj1442  29906  bnj1450  29907  bnj1463  29912  bnj1529  29927  cvmliftlem5  30060  cvmliftlem7  30062  cvmliftlem10  30065  cvmliftlem11  30066  cvmliftlem15  30069  cvmlift2lem11  30084  cvmlift2lem12  30085  ghomgrplem  30355  eldm3  30450  funsseq  30457  frr3g  30561  frrlem1  30562  frrlem4  30565  finixpnum  31974  poimirlem3  31987  poimirlem4  31988  poimirlem9  31993  sdclem2  32115  prdsbnd2  32171  dibffval  34752  hdmapffval  35441  hdmapfval  35442  eldiophb  35643  diophrw  35645  diophin  35659  rclexi  36266  rtrclex  36268  rtrclexi  36272  cnvrcl0  36276  dfrtrcl5  36280  dfrcl2  36310  fvmptiunrelexplb0da  36321  sblpnf  36701  fresin2  37473  cncfuni  37801  dvresntr  37825  dvbdfbdioolem1  37837  itgiccshift  37894  itgperiod  37895  dirkercncflem2  38003  fourierdlem46  38053  fourierdlem48  38055  fourierdlem49  38056  fourierdlem58  38065  fourierdlem72  38079  fourierdlem74  38081  fourierdlem75  38082  fourierdlem81  38088  fourierdlem88  38095  fourierdlem89  38096  fourierdlem90  38097  fourierdlem91  38098  fourierdlem92  38099  fourierdlem103  38110  fourierdlem104  38111  fourierdlem112  38119  fouriersw  38132  voncmpl  38480  funcoressn  38665  resresdm  39049  egrsubgr  39398  pthdlem1  39791  usgra2pthspth  39937  idfusubc0  40137  idfusubc  40138  rngcval  40236  rnghmsubcsetclem1  40249  rngccat  40252  rngcid  40253  rngcidALTV  40265  rngcifuestrc  40271  funcrngcsetc  40272  funcrngcsetcALT  40273  ringcval  40282  rhmsubcsetclem1  40295  ringccat  40298  ringcid  40299  rhmsubcrngclem1  40301  rhmsubcrngc  40303  funcringcsetc  40309  funcringcsetcALTV2lem5  40314  ringcidALTV  40328  funcringcsetclem5ALTV  40337  rhmsubc  40364  rhmsubcALTVlem3  40381  aacllem  40812