Theorem reseq2d 5271

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

Syntax hints:   -> wi 4   = wceq 1379   |` cres 5001

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483  df-opab 4506  df-xp 5005  df-res 5011

This theorem is referenced by:  reseq12d  5272  resima2  5305  resdmdfsn  5317  relresfld  5532  f1orescnv  5829  funcocnv2  5838  fococnv2  5839  fnressn  6071  fnsnsplit  6096  oprssov  6426  curry1  6872  curry2  6875  dftpos2  6969  tfrlem16  7059  sbthlem4  7627  mapunen  7683  hartogslem1  7963  axdc3lem2  8827  fseq1p1m1  11748  hashf1lem1  12466  setsval  14510  idfuval  15099  idfu2nd  15100  resf1st  15117  setcid  15267  catcisolem  15287  1stfval  15314  1stf2  15316  2ndfval  15317  2ndf2  15319  1stfcl  15320  2ndfcl  15321  curf2ndf  15370  hofcl  15382  isps  15685  cnvps  15695  isdir  15715  dirref  15718  tsrdir  15721  frmdval  15842  frmdplusg  15845  gsum2dlem2  16789  gsum2dOLD  16791  dprd2da  16881  dpjval  16895  ablfac1eulem  16913  ablfac1eu  16914  psrplusg  17805  opsrtoslem2  17920  mdetunilem3  18883  mdetunilem4  18884  mdetunilem9  18889  imacmp  19663  ptuncnv  20043  tgphaus  20350  tsmsresOLD  20380  tsmsres  20381  tsmsxplem1  20390  tsmsxplem2  20391  trust  20467  metreslem  20600  imasdsf1olem  20611  xmspropd  20711  mspropd  20712  imasf1oxms  20727  imasf1oms  20728  nmpropd2  20850  isngp2  20852  ngppropd  20886  tngngp2  20901  cmspropd  21523  mbfres2  21787  limciun  22033  dvmptres3  22094  dvmptres2  22100  dvmptntr  22109  dvlipcn  22130  dvlip2  22131  c1liplem1  22132  dvgt0lem1  22138  lhop1lem  22149  dvcnvrelem1  22153  dvcvx  22156  ftc2ditglem  22181  wilthlem2  23071  dchrval  23237  dchrelbas2  23240  ausisusgraedg  24032  1pthonlem1  24267  constr2pth  24279  eupath2lem3  24655  eupath2  24656  efghgrp  25051  drngoi  25085  isdivrngo  25109  hhssablo  25855  hhssnvt  25857  hhsssh  25861  resf1o  27225  qtophaus  27637  esumcvg  27732  eulerpartlemn  27960  sseqp1  27974  signsvtn0  28167  cvmliftlem5  28374  cvmliftlem7  28376  cvmliftlem10  28379  cvmliftlem11  28380  cvmliftlem15  28383  cvmlift2lem11  28398  cvmlift2lem12  28399  ghomgrplem  28504  relexp0  28527  relexpsucr  28528  dfrtrcl2  28546  eldm3  28768  funsseq  28776  wrecseq123  28914  wfr3g  28919  wfrlem1  28920  wfrlem4  28923  wfrlem14  28933  wfr2  28937  tfrALTlem  28939  tfr2ALT  28941  tfr3ALT  28942  frr3g  28963  frrlem1  28964  frrlem4  28967  bpolylem  29387  finixpnum  29615  sdclem2  29838  prdsbnd2  29894  eldiophb  30294  diophrw  30296  diophin  30310  sblpnf  30793  fresin2  31026  cncfuni  31225  dvresntr  31246  dvbdfbdioolem1  31258  itgiccshift  31298  itgperiod  31299  dirkercncflem2  31404  fourierdlem46  31453  fourierdlem48  31455  fourierdlem49  31456  fourierdlem58  31465  fourierdlem72  31479  fourierdlem74  31481  fourierdlem75  31482  fourierdlem81  31488  fourierdlem88  31495  fourierdlem89  31496  fourierdlem90  31497  fourierdlem91  31498  fourierdlem92  31499  fourierdlem103  31510  fourierdlem104  31511  fourierdlem112  31519  fouriersw  31532  funcoressn  31679  usgra2pthspth  31820  bnj1385  32970  bnj1326  33161  bnj1321  33162  bnj1442  33184  bnj1450  33185  bnj1463  33190  bnj1529  33205  dibffval  35937  hdmapffval  36626  hdmapfval  36627