Theorem reseq2d 5105

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

Syntax hints:   -> wi 4   = wceq 1649   |` cres 4839

This theorem is referenced by:  reseq12d  5106  resima2  5138  relresfld  5355  f1orescnv  5649  funcocnv2  5659  fococnv2  5660  fnressn  5877  fnsnsplit  5889  oprssov  6174  curry1  6397  curry2  6400  dftpos2  6455  tfrlem16  6613  sbthlem4  7179  mapunen  7235  hartogslem1  7467  axdc3lem2  8287  fseq1p1m1  11077  hashf1lem1  11659  setsval  13448  idfuval  14028  idfu2nd  14029  resf1st  14046  setcid  14196  catcisolem  14216  1stfval  14243  1stf2  14245  2ndfval  14246  2ndf2  14248  1stfcl  14249  2ndfcl  14250  curf2ndf  14299  hofcl  14311  isps  14589  cnvps  14599  isdir  14632  dirref  14635  tsrdir  14638  frmdval  14751  frmdplusg  14754  gsum2d  15501  dprd2da  15555  dpjval  15569  ablfac1eulem  15585  ablfac1eu  15586  psrplusg  16400  opsrtoslem2  16500  imacmp  17414  ptuncnv  17792  tgphaus  18099  tsmsres  18126  tsmsxplem1  18135  tsmsxplem2  18136  trust  18212  metreslem  18345  imasdsf1olem  18356  xmspropd  18456  mspropd  18457  imasf1oxms  18472  imasf1oms  18473  nmpropd2  18595  isngp2  18597  ngppropd  18631  tngngp2  18646  cmspropd  19255  mbfres2  19490  limciun  19734  dvmptres3  19795  dvmptres2  19801  dvmptntr  19810  dvlipcn  19831  dvlip2  19832  c1liplem1  19833  dvgt0lem1  19839  lhop1lem  19850  dvcnvrelem1  19854  dvcvx  19857  ftc2ditglem  19882  wilthlem2  20805  dchrval  20971  dchrelbas2  20974  1pthonlem1  21542  constr2pth  21554  eupath2lem3  21654  eupath2  21655  efghgrp  21914  drngoi  21948  isdivrngo  21972  hhssablo  22716  hhssnvt  22718  hhsssh  22722  esumcvg  24429  cvmliftlem5  24929  cvmliftlem7  24931  cvmliftlem10  24934  cvmliftlem11  24935  cvmliftlem15  24938  cvmlift2lem11  24953  cvmlift2lem12  24954  ghomgrplem  25053  relexp0  25082  relexpsucr  25083  dfrtrcl2  25101  eldm3  25333  funsseq  25339  wfr3g  25469  wfrlem1  25470  wfrlem4  25473  wfrlem14  25483  wfr2  25487  wfr2c  25488  tfrALTlem  25490  tfr2ALT  25492  tfr3ALT  25493  frr3g  25494  frrlem1  25495  frrlem4  25498  bpolylem  25998  bpolyval  25999  sdclem2  26336  prdsbnd2  26394  eldiophb  26705  diophrw  26707  diophin  26721  sblpnf  27407  funcoressn  27858  usgra2pthspth  28035  bnj1385  28910  bnj1326  29101  bnj1321  29102  bnj1442  29124  bnj1450  29125  bnj1463  29130  bnj1529  29145  dibffval  31623  hdmapffval  32312  hdmapfval  32313

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-in 3287  df-opab 4227  df-xp 4843  df-res 4849