Theorem reseq2d 5396

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

Syntax hints:   -> wi 4   = wceq 1483   |` cres 5116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-opab 4713  df-xp 5120  df-res 5126

This theorem is referenced by:  reseq12d  5397  resima2OLD  5433  resresdm  5626  relresfld  5662  f1orescnv  6152  fococnv2  6162  fvn0ssdmfun  6350  fnressn  6425  fnsnsplit  6450  oprssov  6803  curry1  7269  curry2  7272  dftpos2  7369  wrecseq123  7408  wfr3g  7413  wfrlem1  7414  wfrlem4  7418  wfrlem14  7428  wfr2a  7432  dfrecs3  7469  tfrlem16  7489  tfr2ALT  7497  tfr3ALT  7498  sbthlem4  8073  mapunen  8129  hartogslem1  8447  axdc3lem2  9273  fseq1p1m1  12414  resunimafz0  13229  hashf1lem1  13239  relexp0g  13762  relexp0  13763  relexpsucnnr  13765  dfrtrcl2  13802  bpolylem  14779  setsval  15888  idfuval  16536  idfu2nd  16537  resf1st  16554  setcid  16736  catcisolem  16756  estrcid  16774  funcestrcsetclem5  16784  funcsetcestrclem5  16799  funcsetcestrclem7  16801  1stfval  16831  1stf2  16833  2ndfval  16834  2ndf2  16836  1stfcl  16837  2ndfcl  16838  curf2ndf  16887  hofcl  16899  isps  17202  cnvps  17212  isdir  17232  dirref  17235  tsrdir  17238  frmdval  17388  frmdplusg  17391  gsum2dlem2  18370  dprd2da  18441  dpjval  18455  ablfac1eulem  18471  ablfac1eu  18472  psrplusg  19381  opsrtoslem2  19485  mdetunilem3  20420  mdetunilem4  20421  mdetunilem9  20426  imacmp  21200  ptuncnv  21610  tgphaus  21920  tsmsres  21947  tsmsxplem1  21956  tsmsxplem2  21957  trust  22033  metreslem  22167  imasdsf1olem  22178  xmspropd  22278  mspropd  22279  imasf1oxms  22294  imasf1oms  22295  nmpropd2  22399  isngp2  22401  ngppropd  22441  tngngp2  22456  cmspropd  23146  mbfres2  23412  limciun  23658  dvmptres3  23719  dvmptres2  23725  dvmptntr  23734  dvlipcn  23757  dvlip2  23758  c1liplem1  23759  dvgt0lem1  23765  lhop1lem  23776  dvcnvrelem1  23780  dvcvx  23783  ftc2ditglem  23808  wilthlem2  24795  dchrval  24959  dchrelbas2  24962  egrsubgr  26169  pthdlem1  26662  eupthvdres  27095  eupth2lem3  27096  eupth2  27099  eucrct2eupth  27105  hhssablo  28120  hhssnvt  28122  hhsssh  28126  fnunres1  29417  resf1o  29505  gsummpt2d  29781  qtophaus  29903  esumcvg  30148  eulerpartlemn  30443  sseqp1  30457  signsvtn0  30647  ftc2re  30676  reprsuc  30693  bnj1385  30903  bnj1326  31094  bnj1321  31095  bnj1442  31117  bnj1450  31118  bnj1463  31123  bnj1529  31138  cvmliftlem5  31271  cvmliftlem7  31273  cvmliftlem10  31276  cvmliftlem11  31277  cvmliftlem15  31280  cvmlift2lem11  31295  cvmlift2lem12  31296  eldm3  31651  funsseq  31666  frr3g  31779  frrlem1  31780  frrlem4  31783  noresle  31846  nosupno  31849  nosupdm  31850  nosupfv  31852  nosupres  31853  nosupbnd1lem1  31854  nosupbnd1lem3  31856  nosupbnd1lem5  31858  nosupbnd1  31860  nosupbnd2  31862  noeta  31868  finixpnum  33394  poimirlem3  33412  poimirlem4  33413  poimirlem9  33418  sdclem2  33538  prdsbnd2  33594  isdivrngo  33749  drngoi  33750  dibffval  36429  hdmapffval  37118  hdmapfval  37119  eldiophb  37320  diophrw  37322  diophin  37336  rclexi  37922  rtrclex  37924  rtrclexi  37928  cnvrcl0  37932  dfrtrcl5  37936  dfrcl2  37966  fvmptiunrelexplb0da  37977  sblpnf  38509  fresin2  39352  limsupresuz  39935  limsupvaluz  39940  limsupvaluz2  39970  supcnvlimsup  39972  climrescn  39980  liminfresuz  40016  cncfuni  40099  dvresntr  40132  dvbdfbdioolem1  40143  itgiccshift  40196  itgperiod  40197  dirkercncflem2  40321  fourierdlem46  40369  fourierdlem48  40371  fourierdlem49  40372  fourierdlem58  40381  fourierdlem72  40395  fourierdlem74  40397  fourierdlem75  40398  fourierdlem81  40404  fourierdlem88  40411  fourierdlem89  40412  fourierdlem90  40413  fourierdlem91  40414  fourierdlem92  40415  fourierdlem103  40426  fourierdlem104  40427  fourierdlem112  40435  fouriersw  40448  voncmpl  40835  funcoressn  41207  idfusubc0  41865  idfusubc  41866  rngcval  41962  rnghmsubcsetclem1  41975  rngccat  41978  rngcid  41979  rngcidALTV  41991  rngcifuestrc  41997  funcrngcsetc  41998  funcrngcsetcALT  41999  ringcval  42008  rhmsubcsetclem1  42021  ringccat  42024  ringcid  42025  rhmsubcrngclem1  42027  rhmsubcrngc  42029  funcringcsetc  42035  funcringcsetcALTV2lem5  42040  ringcidALTV  42054  funcringcsetclem5ALTV  42063  rhmsubc  42090  rhmsubcALTVlem3  42106  aacllem  42547