Theorem reseq2d 5981

Description: Equality deduction for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypothesis

Ref	Expression
reseqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
reseq2d	⊢ (𝜑 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Proof of Theorem reseq2d

Step	Hyp	Ref	Expression
1		reseqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		reseq2 5976	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1534   ↾ cres 5676

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420  df-in 3953  df-opab 5208  df-xp 5680  df-res 5686

This theorem is referenced by:  reseq12d  5982  resresdm  6236  relresfld  6279  fnunres1  6664  f1orescnv  6850  fococnv2  6861  fvn0ssdmfun  7080  fnressn  7164  fnsnsplit  7190  oprssov  7587  curry1  8110  curry2  8113  dftpos2  8250  frecseq123  8289  fpr3g  8292  frrlem1  8293  frrlem4  8296  frrlem12  8304  fpr2a  8309  wrecseq123OLD  8322  wfr3g  8329  wfrlem1OLD  8330  wfrlem4OLD  8334  wfrlem14OLD  8344  wfr2aOLD  8348  dfrecs3  8394  dfrecs3OLD  8395  tfrlem16  8415  tfr2ALT  8423  tfr3ALT  8424  on2recsov  8690  sbthlem4  9116  mapunen  9176  hartogslem1  9578  frr3g  9792  frr2  9796  axdc3lem2  10485  fseq1p1m1  13623  resunimafz0  14457  hashf1lem1  14468  hashf1lem1OLD  14469  relexp0g  15022  relexp0  15023  relexpsucnnr  15025  dfrtrcl2  15062  bpolylem  16045  setsval  17164  idfuval  17890  idfu2nd  17891  resf1st  17908  idfusubc0  17913  idfusubc  17914  setcid  18103  catcisolem  18127  estrcid  18152  funcestrcsetclem5  18163  funcsetcestrclem5  18178  funcsetcestrclem7  18180  1stfval  18210  1stf2  18212  2ndfval  18213  2ndf2  18215  1stfcl  18216  2ndfcl  18217  curf2ndf  18267  hofcl  18279  isps  18588  cnvps  18598  isdir  18618  dirref  18621  tsrdir  18624  frmdval  18836  frmdplusg  18839  gsum2dlem2  19965  dprd2da  20038  dpjval  20052  ablfac1eulem  20068  ablfac1eu  20069  rngcval  20592  rnghmsubcsetclem1  20605  rngccat  20608  rngcid  20609  rngcifuestrc  20613  funcrngcsetc  20614  funcrngcsetcALT  20615  ringcval  20621  rhmsubcsetclem1  20634  ringccat  20637  ringcid  20638  rhmsubcrngclem1  20640  rhmsubcrngc  20642  funcringcsetc  20648  rhmsubc  20663  psrplusg  21941  opsrtoslem2  22065  mdetunilem3  22604  mdetunilem4  22605  mdetunilem9  22610  imacmp  23389  ptuncnv  23799  tgphaus  24109  tsmsres  24136  tsmsxplem1  24145  tsmsxplem2  24146  trust  24222  metreslem  24356  imasdsf1olem  24367  xmspropd  24467  mspropd  24468  imasf1oxms  24486  imasf1oms  24487  nmpropd2  24592  isngp2  24594  ngppropd  24634  tngngp2  24657  cphsscph  25267  cmspropd  25365  cmssmscld  25366  mbfres2  25662  limciun  25911  dvmptres3  25976  dvmptres2  25982  dvmptntr  25991  dvlipcn  26015  dvlip2  26016  c1liplem1  26017  dvgt0lem1  26023  lhop1lem  26034  dvcnvrelem1  26038  dvcvx  26041  ftc2ditglem  26068  wilthlem2  27094  dchrval  27260  dchrelbas2  27263  noresle  27724  nosupcbv  27729  nosupno  27730  nosupdm  27731  nosupfv  27733  nosupres  27734  nosupbnd1lem1  27735  nosupbnd1lem3  27737  nosupbnd1lem5  27739  nosupbnd1  27741  nosupbnd2  27743  noinfcbv  27744  noinfno  27745  noinfdm  27746  noinffv  27748  noinfres  27749  noinfbnd1lem3  27752  noinfbnd1lem5  27754  noinfbnd1  27756  noinfbnd2  27758  noetalem1  27768  norecov  27958  norec2ov  27968  egrsubgr  29210  pthdlem1  29700  eupthvdres  30165  eupth2lem3  30166  eupth2  30169  eucrct2eupth  30175  hhssablo  31193  hhssnvt  31195  hhsssh  31199  fressupp  32600  resf1o  32644  gsummpt2d  32921  gsumpart  32927  symgcom  32965  tocycval  32990  tocycfv  32991  tocycf  32999  tocyc01  33000  cycpm2tr  33001  cycpmconjslem1  33036  cycpmconjslem2  33037  nsgqusf1o  33297  qtophaus  33664  esumcvg  33932  eulerpartlemn  34228  sseqp1  34242  signsvtn0  34429  ftc2re  34457  reprsuc  34474  bnj1385  34690  bnj1326  34884  bnj1321  34885  bnj1442  34907  bnj1450  34908  bnj1463  34913  bnj1529  34928  f1resfz0f1d  34954  pfxwlk  34964  pthhashvtx  34968  cvmliftlem5  35130  cvmliftlem7  35132  cvmliftlem10  35135  cvmliftlem11  35136  cvmliftlem15  35139  cvmlift2lem11  35154  cvmlift2lem12  35155  satffunlem1lem1  35243  satffunlem2lem1  35245  eldm3  35596  funsseq  35604  finixpnum  37319  poimirlem3  37337  poimirlem4  37338  poimirlem9  37343  sdclem2  37456  prdsbnd2  37509  isdivrngo  37664  drngoi  37665  elrefsymrels2  38280  eleqvrels2  38303  dibffval  40852  hdmapffval  41538  hdmapfval  41539  eqresfnbd  41978  eldiophb  42451  diophrw  42453  diophin  42466  tfsconcatrev  43051  ofoafg  43057  resisoeq45d  43124  rclexi  43319  rtrclex  43321  rtrclexi  43325  cnvrcl0  43329  dfrtrcl5  43333  dfrcl2  43378  fvmptiunrelexplb0da  43389  sblpnf  44021  fresin2  44815  limsupresuz  45360  limsupvaluz  45365  limsupvaluz2  45395  supcnvlimsup  45397  climrescn  45405  liminfresuz  45441  cncfuni  45543  dvresntr  45575  dvbdfbdioolem1  45585  itgiccshift  45637  itgperiod  45638  dirkercncflem2  45761  fourierdlem46  45809  fourierdlem48  45811  fourierdlem49  45812  fourierdlem58  45821  fourierdlem72  45835  fourierdlem74  45837  fourierdlem75  45838  fourierdlem81  45844  fourierdlem88  45851  fourierdlem89  45852  fourierdlem90  45853  fourierdlem91  45854  fourierdlem92  45855  fourierdlem103  45866  fourierdlem104  45867  fourierdlem112  45875  fouriersw  45888  voncmpl  46278  funcoressn  46693  funressnmo  46697  f1cof1blem  46725  funfocofob  46727  funressndmafv2rn  46872  f1oresf1orab  46938  isubgrgrim  47512  rngcidALTV  47687  rhmsubcALTVlem3  47696  funcringcsetcALTV2lem5  47707  ringcidALTV  47721  funcringcsetclem5ALTV  47730  itcoval  48085  itcoval0mpt  48090  itcovalendof  48093  aacllem  48585