Theorem reseq2d 5894

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

Syntax hints:   → wi 4   = wceq 1539   ↾ cres 5592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-in 3895  df-opab 5138  df-xp 5596  df-res 5602

This theorem is referenced by:  reseq12d  5895  resresdm  6141  relresfld  6183  f1orescnv  6740  fococnv2  6751  fvn0ssdmfun  6961  fnressn  7039  fnsnsplit  7065  oprssov  7450  curry1  7953  curry2  7956  dftpos2  8068  frecseq123  8107  fpr3g  8110  frrlem1  8111  frrlem4  8114  frrlem12  8122  fpr2a  8127  wrecseq123OLD  8140  wfr3g  8147  wfrlem1OLD  8148  wfrlem4OLD  8152  wfrlem14OLD  8162  wfr2aOLD  8166  dfrecs3  8212  dfrecs3OLD  8213  tfrlem16  8233  tfr2ALT  8241  tfr3ALT  8242  sbthlem4  8882  mapunen  8942  hartogslem1  9310  frr3g  9523  frr2  9527  axdc3lem2  10216  fseq1p1m1  13339  resunimafz0  14166  hashf1lem1  14177  hashf1lem1OLD  14178  relexp0g  14742  relexp0  14743  relexpsucnnr  14745  dfrtrcl2  14782  bpolylem  15767  setsval  16877  idfuval  17600  idfu2nd  17601  resf1st  17618  setcid  17810  catcisolem  17834  estrcid  17859  funcestrcsetclem5  17870  funcsetcestrclem5  17885  funcsetcestrclem7  17887  1stfval  17917  1stf2  17919  2ndfval  17920  2ndf2  17922  1stfcl  17923  2ndfcl  17924  curf2ndf  17974  hofcl  17986  isps  18295  cnvps  18305  isdir  18325  dirref  18328  tsrdir  18331  frmdval  18499  frmdplusg  18502  gsum2dlem2  19581  dprd2da  19654  dpjval  19668  ablfac1eulem  19684  ablfac1eu  19685  psrplusg  21159  opsrtoslem2  21272  mdetunilem3  21772  mdetunilem4  21773  mdetunilem9  21778  imacmp  22557  ptuncnv  22967  tgphaus  23277  tsmsres  23304  tsmsxplem1  23313  tsmsxplem2  23314  trust  23390  metreslem  23524  imasdsf1olem  23535  xmspropd  23635  mspropd  23636  imasf1oxms  23654  imasf1oms  23655  nmpropd2  23760  isngp2  23762  ngppropd  23802  tngngp2  23825  cphsscph  24424  cmspropd  24522  cmssmscld  24523  mbfres2  24818  limciun  25067  dvmptres3  25129  dvmptres2  25135  dvmptntr  25144  dvlipcn  25167  dvlip2  25168  c1liplem1  25169  dvgt0lem1  25175  lhop1lem  25186  dvcnvrelem1  25190  dvcvx  25193  ftc2ditglem  25218  wilthlem2  26227  dchrval  26391  dchrelbas2  26394  egrsubgr  27653  pthdlem1  28143  eupthvdres  28608  eupth2lem3  28609  eupth2  28612  eucrct2eupth  28618  hhssablo  29634  hhssnvt  29636  hhsssh  29640  fnunres1  30954  fressupp  31031  resf1o  31074  gsummpt2d  31318  gsumpart  31324  symgcom  31361  tocycval  31384  tocycfv  31385  tocycf  31393  tocyc01  31394  cycpm2tr  31395  cycpmconjslem1  31430  cycpmconjslem2  31431  nsgqusf1o  31610  qtophaus  31795  esumcvg  32063  eulerpartlemn  32357  sseqp1  32371  signsvtn0  32558  ftc2re  32587  reprsuc  32604  bnj1385  32821  bnj1326  33015  bnj1321  33016  bnj1442  33038  bnj1450  33039  bnj1463  33044  bnj1529  33059  f1resfz0f1d  33081  pfxwlk  33094  pthhashvtx  33098  cvmliftlem5  33260  cvmliftlem7  33262  cvmliftlem10  33265  cvmliftlem11  33266  cvmliftlem15  33269  cvmlift2lem11  33284  cvmlift2lem12  33285  satffunlem1lem1  33373  satffunlem2lem1  33375  eldm3  33737  funsseq  33751  on2recsov  33836  noresle  33909  nosupcbv  33914  nosupno  33915  nosupdm  33916  nosupfv  33918  nosupres  33919  nosupbnd1lem1  33920  nosupbnd1lem3  33922  nosupbnd1lem5  33924  nosupbnd1  33926  nosupbnd2  33928  noinfcbv  33929  noinfno  33930  noinfdm  33931  noinffv  33933  noinfres  33934  noinfbnd1lem3  33937  noinfbnd1lem5  33939  noinfbnd1  33941  noinfbnd2  33943  noetalem1  33953  norecov  34113  norec2ov  34123  finixpnum  35771  poimirlem3  35789  poimirlem4  35790  poimirlem9  35795  sdclem2  35909  prdsbnd2  35962  isdivrngo  36117  drngoi  36118  elrefsymrels2  36690  eleqvrels2  36712  dibffval  39161  hdmapffval  39847  hdmapfval  39848  eldiophb  40586  diophrw  40588  diophin  40601  rclexi  41230  rtrclex  41232  rtrclexi  41236  cnvrcl0  41240  dfrtrcl5  41244  dfrcl2  41289  fvmptiunrelexplb0da  41300  sblpnf  41935  fresin2  42715  limsupresuz  43251  limsupvaluz  43256  limsupvaluz2  43286  supcnvlimsup  43288  climrescn  43296  liminfresuz  43332  cncfuni  43434  dvresntr  43466  dvbdfbdioolem1  43476  itgiccshift  43528  itgperiod  43529  dirkercncflem2  43652  fourierdlem46  43700  fourierdlem48  43702  fourierdlem49  43703  fourierdlem58  43712  fourierdlem72  43726  fourierdlem74  43728  fourierdlem75  43729  fourierdlem81  43735  fourierdlem88  43742  fourierdlem89  43743  fourierdlem90  43744  fourierdlem91  43745  fourierdlem92  43746  fourierdlem103  43757  fourierdlem104  43758  fourierdlem112  43766  fouriersw  43779  voncmpl  44166  funcoressn  44547  funressnmo  44551  f1cof1blem  44579  funfocofob  44581  funressndmafv2rn  44726  f1oresf1orab  44792  isomgreqve  45288  idfusubc0  45434  idfusubc  45435  rngcval  45531  rnghmsubcsetclem1  45544  rngccat  45547  rngcid  45548  rngcidALTV  45560  rngcifuestrc  45566  funcrngcsetc  45567  funcrngcsetcALT  45568  ringcval  45577  rhmsubcsetclem1  45590  ringccat  45593  ringcid  45594  rhmsubcrngclem1  45596  rhmsubcrngc  45598  funcringcsetc  45604  funcringcsetcALTV2lem5  45609  ringcidALTV  45623  funcringcsetclem5ALTV  45632  rhmsubc  45659  rhmsubcALTVlem3  45675  itcoval  46018  itcoval0mpt  46023  itcovalendof  46026  aacllem  46516