Theorem reseq2d 5979

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 5974	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1541   ↾ cres 5677

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-in 3954  df-opab 5210  df-xp 5681  df-res 5687

This theorem is referenced by:  reseq12d  5980  resresdm  6229  relresfld  6272  fnunres1  6658  f1orescnv  6845  fococnv2  6856  fvn0ssdmfun  7073  fnressn  7152  fnsnsplit  7178  oprssov  7572  curry1  8086  curry2  8089  dftpos2  8224  frecseq123  8263  fpr3g  8266  frrlem1  8267  frrlem4  8270  frrlem12  8278  fpr2a  8283  wrecseq123OLD  8296  wfr3g  8303  wfrlem1OLD  8304  wfrlem4OLD  8308  wfrlem14OLD  8318  wfr2aOLD  8322  dfrecs3  8368  dfrecs3OLD  8369  tfrlem16  8389  tfr2ALT  8397  tfr3ALT  8398  on2recsov  8663  sbthlem4  9082  mapunen  9142  hartogslem1  9533  frr3g  9747  frr2  9751  axdc3lem2  10442  fseq1p1m1  13571  resunimafz0  14400  hashf1lem1  14411  hashf1lem1OLD  14412  relexp0g  14965  relexp0  14966  relexpsucnnr  14968  dfrtrcl2  15005  bpolylem  15988  setsval  17096  idfuval  17822  idfu2nd  17823  resf1st  17840  setcid  18032  catcisolem  18056  estrcid  18081  funcestrcsetclem5  18092  funcsetcestrclem5  18107  funcsetcestrclem7  18109  1stfval  18139  1stf2  18141  2ndfval  18142  2ndf2  18144  1stfcl  18145  2ndfcl  18146  curf2ndf  18196  hofcl  18208  isps  18517  cnvps  18527  isdir  18547  dirref  18550  tsrdir  18553  frmdval  18728  frmdplusg  18731  gsum2dlem2  19833  dprd2da  19906  dpjval  19920  ablfac1eulem  19936  ablfac1eu  19937  psrplusg  21491  opsrtoslem2  21608  mdetunilem3  22107  mdetunilem4  22108  mdetunilem9  22113  imacmp  22892  ptuncnv  23302  tgphaus  23612  tsmsres  23639  tsmsxplem1  23648  tsmsxplem2  23649  trust  23725  metreslem  23859  imasdsf1olem  23870  xmspropd  23970  mspropd  23971  imasf1oxms  23989  imasf1oms  23990  nmpropd2  24095  isngp2  24097  ngppropd  24137  tngngp2  24160  cphsscph  24759  cmspropd  24857  cmssmscld  24858  mbfres2  25153  limciun  25402  dvmptres3  25464  dvmptres2  25470  dvmptntr  25479  dvlipcn  25502  dvlip2  25503  c1liplem1  25504  dvgt0lem1  25510  lhop1lem  25521  dvcnvrelem1  25525  dvcvx  25528  ftc2ditglem  25553  wilthlem2  26562  dchrval  26726  dchrelbas2  26729  noresle  27189  nosupcbv  27194  nosupno  27195  nosupdm  27196  nosupfv  27198  nosupres  27199  nosupbnd1lem1  27200  nosupbnd1lem3  27202  nosupbnd1lem5  27204  nosupbnd1  27206  nosupbnd2  27208  noinfcbv  27209  noinfno  27210  noinfdm  27211  noinffv  27213  noinfres  27214  noinfbnd1lem3  27217  noinfbnd1lem5  27219  noinfbnd1  27221  noinfbnd2  27223  noetalem1  27233  norecov  27420  norec2ov  27430  egrsubgr  28523  pthdlem1  29012  eupthvdres  29477  eupth2lem3  29478  eupth2  29481  eucrct2eupth  29487  hhssablo  30503  hhssnvt  30505  hhsssh  30509  fressupp  31897  resf1o  31942  gsummpt2d  32188  gsumpart  32194  symgcom  32231  tocycval  32254  tocycfv  32255  tocycf  32263  tocyc01  32264  cycpm2tr  32265  cycpmconjslem1  32300  cycpmconjslem2  32301  nsgqusf1o  32515  qtophaus  32804  esumcvg  33072  eulerpartlemn  33368  sseqp1  33382  signsvtn0  33569  ftc2re  33598  reprsuc  33615  bnj1385  33831  bnj1326  34025  bnj1321  34026  bnj1442  34048  bnj1450  34049  bnj1463  34054  bnj1529  34069  f1resfz0f1d  34091  pfxwlk  34102  pthhashvtx  34106  cvmliftlem5  34268  cvmliftlem7  34270  cvmliftlem10  34273  cvmliftlem11  34274  cvmliftlem15  34277  cvmlift2lem11  34292  cvmlift2lem12  34293  satffunlem1lem1  34381  satffunlem2lem1  34383  eldm3  34719  funsseq  34727  finixpnum  36461  poimirlem3  36479  poimirlem4  36480  poimirlem9  36485  sdclem2  36598  prdsbnd2  36651  isdivrngo  36806  drngoi  36807  elrefsymrels2  37427  eleqvrels2  37450  dibffval  39999  hdmapffval  40685  hdmapfval  40686  eqresfnbd  41051  eldiophb  41480  diophrw  41482  diophin  41495  tfsconcatrev  42083  ofoafg  42089  resisoeq45d  42156  rclexi  42351  rtrclex  42353  rtrclexi  42357  cnvrcl0  42361  dfrtrcl5  42365  dfrcl2  42410  fvmptiunrelexplb0da  42421  sblpnf  43054  fresin2  43853  limsupresuz  44405  limsupvaluz  44410  limsupvaluz2  44440  supcnvlimsup  44442  climrescn  44450  liminfresuz  44486  cncfuni  44588  dvresntr  44620  dvbdfbdioolem1  44630  itgiccshift  44682  itgperiod  44683  dirkercncflem2  44806  fourierdlem46  44854  fourierdlem48  44856  fourierdlem49  44857  fourierdlem58  44866  fourierdlem72  44880  fourierdlem74  44882  fourierdlem75  44883  fourierdlem81  44889  fourierdlem88  44896  fourierdlem89  44897  fourierdlem90  44898  fourierdlem91  44899  fourierdlem92  44900  fourierdlem103  44911  fourierdlem104  44912  fourierdlem112  44920  fouriersw  44933  voncmpl  45323  funcoressn  45738  funressnmo  45742  f1cof1blem  45770  funfocofob  45772  funressndmafv2rn  45917  f1oresf1orab  45983  isomgreqve  46479  idfusubc0  46625  idfusubc  46626  rngcval  46813  rnghmsubcsetclem1  46826  rngccat  46829  rngcid  46830  rngcidALTV  46842  rngcifuestrc  46848  funcrngcsetc  46849  funcrngcsetcALT  46850  ringcval  46859  rhmsubcsetclem1  46872  ringccat  46875  ringcid  46876  rhmsubcrngclem1  46878  rhmsubcrngc  46880  funcringcsetc  46886  funcringcsetcALTV2lem5  46891  ringcidALTV  46905  funcringcsetclem5ALTV  46914  rhmsubc  46941  rhmsubcALTVlem3  46957  itcoval  47300  itcoval0mpt  47305  itcovalendof  47308  aacllem  47801