Theorem reseq2d 5263

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

Syntax hints:   -> wi 4   = wceq 1383   |` cres 4991

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-in 3468  df-opab 4496  df-xp 4995  df-res 5001

This theorem is referenced by:  reseq12d  5264  resima2  5297  resdmdfsn  5309  relresfld  5524  f1orescnv  5821  funcocnv2  5830  fococnv2  5831  fvn0ssdmfun  6007  fnressn  6068  fnsnsplit  6093  oprssov  6429  curry1  6877  curry2  6880  dftpos2  6974  tfrlem16  7064  sbthlem4  7632  mapunen  7688  hartogslem1  7970  axdc3lem2  8834  fseq1p1m1  11761  hashf1lem1  12483  setsval  14533  idfuval  15119  idfu2nd  15120  resf1st  15137  setcid  15287  catcisolem  15307  1stfval  15334  1stf2  15336  2ndfval  15337  2ndf2  15339  1stfcl  15340  2ndfcl  15341  curf2ndf  15390  hofcl  15402  isps  15706  cnvps  15716  isdir  15736  dirref  15739  tsrdir  15742  frmdval  15893  frmdplusg  15896  gsum2dlem2  16872  gsum2dOLD  16874  dprd2da  16965  dpjval  16979  ablfac1eulem  16997  ablfac1eu  16998  psrplusg  17908  opsrtoslem2  18023  mdetunilem3  18989  mdetunilem4  18990  mdetunilem9  18995  imacmp  19770  ptuncnv  20181  tgphaus  20488  tsmsresOLD  20518  tsmsres  20519  tsmsxplem1  20528  tsmsxplem2  20529  trust  20605  metreslem  20738  imasdsf1olem  20749  xmspropd  20849  mspropd  20850  imasf1oxms  20865  imasf1oms  20866  nmpropd2  20988  isngp2  20990  ngppropd  21024  tngngp2  21039  cmspropd  21661  mbfres2  21925  limciun  22171  dvmptres3  22232  dvmptres2  22238  dvmptntr  22247  dvlipcn  22268  dvlip2  22269  c1liplem1  22270  dvgt0lem1  22276  lhop1lem  22287  dvcnvrelem1  22291  dvcvx  22294  ftc2ditglem  22319  wilthlem2  23215  dchrval  23381  dchrelbas2  23384  ausisusgraedg  24228  1pthonlem1  24463  constr2pth  24475  eupath2lem3  24851  eupath2  24852  efghgrpOLD  25247  drngoi  25281  isdivrngo  25305  hhssablo  26051  hhssnvt  26053  hhsssh  26057  resf1o  27425  qtophaus  27712  esumcvg  27965  eulerpartlemn  28193  sseqp1  28207  signsvtn0  28400  cvmliftlem5  28607  cvmliftlem7  28609  cvmliftlem10  28612  cvmliftlem11  28613  cvmliftlem15  28616  cvmlift2lem11  28631  cvmlift2lem12  28632  ghomgrplem  28902  relexp0  28925  relexpsucr  28926  dfrtrcl2  28944  eldm3  29166  funsseq  29174  wrecseq123  29312  wfr3g  29317  wfrlem1  29318  wfrlem4  29321  wfrlem14  29331  wfr2  29335  tfrALTlem  29337  tfr2ALT  29339  tfr3ALT  29340  frr3g  29361  frrlem1  29362  frrlem4  29365  bpolylem  29785  finixpnum  30013  sdclem2  30210  prdsbnd2  30266  eldiophb  30665  diophrw  30667  diophin  30681  sblpnf  31166  fresin2  31398  cncfuni  31596  dvresntr  31617  dvbdfbdioolem1  31629  itgiccshift  31669  itgperiod  31670  dirkercncflem2  31775  fourierdlem46  31824  fourierdlem48  31826  fourierdlem49  31827  fourierdlem58  31836  fourierdlem72  31850  fourierdlem74  31852  fourierdlem75  31853  fourierdlem81  31859  fourierdlem88  31866  fourierdlem89  31867  fourierdlem90  31868  fourierdlem91  31869  fourierdlem92  31870  fourierdlem103  31881  fourierdlem104  31882  fourierdlem112  31890  fouriersw  31903  funcoressn  32050  usgra2pthspth  32189  idfusubc0  32398  idfusubc  32399  estrcid  32489  funcestrcsetclem5  32499  rngcval  32510  rnghmsubcsetclem1  32523  rngccat  32526  rngcid  32527  rngcidOLD  32539  rngcifuestrc  32545  funcrngcsetc  32546  funcrngcsetcALT  32547  ringcval  32553  rhmsubcsetclem1  32566  ringccat  32569  ringcid  32570  rhmsubcrngclem1  32572  rhmsubcrngc  32574  funcringcsetc  32580  funcringcsetcOLD2lem5  32585  ringcidOLD  32599  funcringcsetclem5OLD  32608  rhmsubc  32631  rhmsubcOLDlem3  32648  bnj1385  33624  bnj1326  33815  bnj1321  33816  bnj1442  33838  bnj1450  33839  bnj1463  33844  bnj1529  33859  dibffval  36607  hdmapffval  37296  hdmapfval  37297