Theorem reseq2d 5934

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

Syntax hints:   → wi 4   = wceq 1540   ↾ cres 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-in 3912  df-opab 5158  df-xp 5629  df-res 5635

This theorem is referenced by:  reseq12d  5935  imadifssran  6104  resresdm  6186  relresfld  6228  fnunres1  6598  f1orescnv  6783  fococnv2  6794  fvn0ssdmfun  7012  fnressn  7096  fnsnsplit  7124  oprssov  7522  curry1  8044  curry2  8047  dftpos2  8183  frecseq123  8222  fpr3g  8225  frrlem1  8226  frrlem4  8229  frrlem12  8237  fpr2a  8242  wfr3g  8259  dfrecs3  8302  tfrlem16  8322  tfr2ALT  8330  tfr3ALT  8331  on2recsov  8593  sbthlem4  9014  mapunen  9070  hartogslem1  9453  frr3g  9671  frr2  9675  axdc3lem2  10364  fseq1p1m1  13519  resunimafz0  14370  hashf1lem1  14380  relexp0g  14947  relexp0  14948  relexpsucnnr  14950  dfrtrcl2  14987  bpolylem  15973  setsval  17096  idfuval  17801  idfu2nd  17802  resf1st  17819  idfusubc0  17824  idfusubc  17825  setcid  18011  catcisolem  18035  estrcid  18058  funcestrcsetclem5  18068  funcsetcestrclem5  18083  funcsetcestrclem7  18085  1stfval  18115  1stf2  18117  2ndfval  18118  2ndf2  18120  1stfcl  18121  2ndfcl  18122  curf2ndf  18171  hofcl  18183  isps  18492  cnvps  18502  isdir  18522  dirref  18525  tsrdir  18528  frmdval  18743  frmdplusg  18746  gsum2dlem2  19868  dprd2da  19941  dpjval  19955  ablfac1eulem  19971  ablfac1eu  19972  rngcval  20521  rnghmsubcsetclem1  20534  rngccat  20537  rngcid  20538  rngcifuestrc  20542  funcrngcsetc  20543  funcrngcsetcALT  20544  ringcval  20550  rhmsubcsetclem1  20563  ringccat  20566  ringcid  20567  rhmsubcrngclem1  20569  rhmsubcrngc  20571  funcringcsetc  20577  rhmsubc  20592  psrplusg  21861  opsrtoslem2  21979  mdetunilem3  22517  mdetunilem4  22518  mdetunilem9  22523  imacmp  23300  ptuncnv  23710  tgphaus  24020  tsmsres  24047  tsmsxplem1  24056  tsmsxplem2  24057  trust  24133  metreslem  24266  imasdsf1olem  24277  xmspropd  24377  mspropd  24378  imasf1oxms  24393  imasf1oms  24394  nmpropd2  24499  isngp2  24501  ngppropd  24541  tngngp2  24556  cphsscph  25167  cmspropd  25265  cmssmscld  25266  mbfres2  25562  limciun  25811  dvmptres3  25876  dvmptres2  25882  dvmptntr  25891  dvlipcn  25915  dvlip2  25916  c1liplem1  25917  dvgt0lem1  25923  lhop1lem  25934  dvcnvrelem1  25938  dvcvx  25941  ftc2ditglem  25968  wilthlem2  26995  dchrval  27161  dchrelbas2  27164  noresle  27625  nosupcbv  27630  nosupno  27631  nosupdm  27632  nosupfv  27634  nosupres  27635  nosupbnd1lem1  27636  nosupbnd1lem3  27638  nosupbnd1lem5  27640  nosupbnd1  27642  nosupbnd2  27644  noinfcbv  27645  noinfno  27646  noinfdm  27647  noinffv  27649  noinfres  27650  noinfbnd1lem3  27653  noinfbnd1lem5  27655  noinfbnd1  27657  noinfbnd2  27659  noetalem1  27669  norecov  27877  norec2ov  27887  egrsubgr  29240  dfpth2  29692  pthdlem1  29729  eupthvdres  30197  eupth2lem3  30198  eupth2  30201  eucrct2eupth  30207  hhssablo  31225  hhssnvt  31227  hhsssh  31231  fressupp  32644  resf1o  32686  gsummpt2d  33015  gsumpart  33023  symgcom  33038  tocycval  33063  tocycfv  33064  tocycf  33072  tocyc01  33073  cycpm2tr  33074  cycpmconjslem1  33109  cycpmconjslem2  33110  nsgqusf1o  33363  qtophaus  33802  esumcvg  34052  eulerpartlemn  34348  sseqp1  34362  signsvtn0  34537  ftc2re  34565  reprsuc  34582  bnj1385  34798  bnj1326  34992  bnj1321  34993  bnj1442  35015  bnj1450  35016  bnj1463  35021  bnj1529  35036  f1resfz0f1d  35086  pfxwlk  35096  pthhashvtx  35100  cvmliftlem5  35261  cvmliftlem7  35263  cvmliftlem10  35266  cvmliftlem11  35267  cvmliftlem15  35270  cvmlift2lem11  35285  cvmlift2lem12  35286  satffunlem1lem1  35374  satffunlem2lem1  35376  eldm3  35733  funsseq  35740  finixpnum  37584  poimirlem3  37602  poimirlem4  37603  poimirlem9  37608  sdclem2  37721  prdsbnd2  37774  isdivrngo  37929  drngoi  37930  elrefsymrels2  38545  eleqvrels2  38568  dibffval  41119  hdmapffval  41805  hdmapfval  41806  eqresfnbd  42205  dvun  42332  eldiophb  42730  diophrw  42732  diophin  42745  tfsconcatrev  43321  ofoafg  43327  resisoeq45d  43393  rclexi  43588  rtrclex  43590  rtrclexi  43594  cnvrcl0  43598  dfrtrcl5  43602  dfrcl2  43647  fvmptiunrelexplb0da  43658  sblpnf  44283  fresin2  45150  limsupresuz  45685  limsupvaluz  45690  limsupvaluz2  45720  supcnvlimsup  45722  climrescn  45730  liminfresuz  45766  cncfuni  45868  dvresntr  45900  dvbdfbdioolem1  45910  itgiccshift  45962  itgperiod  45963  dirkercncflem2  46086  fourierdlem46  46134  fourierdlem48  46136  fourierdlem49  46137  fourierdlem58  46146  fourierdlem72  46160  fourierdlem74  46162  fourierdlem75  46163  fourierdlem81  46169  fourierdlem88  46176  fourierdlem89  46177  fourierdlem90  46178  fourierdlem91  46179  fourierdlem92  46180  fourierdlem103  46191  fourierdlem104  46192  fourierdlem112  46200  fouriersw  46213  voncmpl  46603  funcoressn  47027  funressnmo  47031  f1cof1blem  47059  funfocofob  47063  funressndmafv2rn  47208  f1oresf1orab  47274  upgrimpths  47894  isubgrgrim  47914  stgrfv  47938  gpgov  48027  rngcidALTV  48259  rhmsubcALTVlem3  48268  funcringcsetcALTV2lem5  48279  ringcidALTV  48293  funcringcsetclem5ALTV  48302  itcoval  48647  itcoval0mpt  48652  itcovalendof  48655  idfu1sta  49087  idfu2nda  49089  imaidfu2  49097  idfullsubc  49147  dfswapf2  49247  oppc1stf  49274  oppc2ndf  49275  1stfpropd  49276  2ndfpropd  49277  fucofvalg  49304  fucof1  49308  fucofvalne  49311  opf2fval  49391  idfudiag1  49511  aacllem  49787