Theorem reseq2d 5996

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-in 3957  df-opab 5205  df-xp 5690  df-res 5696

This theorem is referenced by:  reseq12d  5997  imadifssran  6170  resresdm  6252  relresfld  6295  fnunres1  6679  f1orescnv  6862  fococnv2  6873  fvn0ssdmfun  7093  fnressn  7177  fnsnsplit  7205  oprssov  7603  curry1  8130  curry2  8133  dftpos2  8269  frecseq123  8308  fpr3g  8311  frrlem1  8312  frrlem4  8315  frrlem12  8323  fpr2a  8328  wrecseq123OLD  8341  wfr3g  8348  wfrlem1OLD  8349  wfrlem4OLD  8353  wfrlem14OLD  8363  wfr2aOLD  8367  dfrecs3  8413  dfrecs3OLD  8414  tfrlem16  8434  tfr2ALT  8442  tfr3ALT  8443  on2recsov  8707  sbthlem4  9127  mapunen  9187  hartogslem1  9583  frr3g  9797  frr2  9801  axdc3lem2  10492  fseq1p1m1  13639  resunimafz0  14485  hashf1lem1  14495  relexp0g  15062  relexp0  15063  relexpsucnnr  15065  dfrtrcl2  15102  bpolylem  16085  setsval  17205  idfuval  17922  idfu2nd  17923  resf1st  17940  idfusubc0  17945  idfusubc  17946  setcid  18132  catcisolem  18156  estrcid  18179  funcestrcsetclem5  18190  funcsetcestrclem5  18205  funcsetcestrclem7  18207  1stfval  18237  1stf2  18239  2ndfval  18240  2ndf2  18242  1stfcl  18243  2ndfcl  18244  curf2ndf  18293  hofcl  18305  isps  18614  cnvps  18624  isdir  18644  dirref  18647  tsrdir  18650  frmdval  18865  frmdplusg  18868  gsum2dlem2  19990  dprd2da  20063  dpjval  20077  ablfac1eulem  20093  ablfac1eu  20094  rngcval  20619  rnghmsubcsetclem1  20632  rngccat  20635  rngcid  20636  rngcifuestrc  20640  funcrngcsetc  20641  funcrngcsetcALT  20642  ringcval  20648  rhmsubcsetclem1  20661  ringccat  20664  ringcid  20665  rhmsubcrngclem1  20667  rhmsubcrngc  20669  funcringcsetc  20675  rhmsubc  20690  psrplusg  21957  opsrtoslem2  22081  mdetunilem3  22621  mdetunilem4  22622  mdetunilem9  22627  imacmp  23406  ptuncnv  23816  tgphaus  24126  tsmsres  24153  tsmsxplem1  24162  tsmsxplem2  24163  trust  24239  metreslem  24373  imasdsf1olem  24384  xmspropd  24484  mspropd  24485  imasf1oxms  24503  imasf1oms  24504  nmpropd2  24609  isngp2  24611  ngppropd  24651  tngngp2  24674  cphsscph  25286  cmspropd  25384  cmssmscld  25385  mbfres2  25681  limciun  25930  dvmptres3  25995  dvmptres2  26001  dvmptntr  26010  dvlipcn  26034  dvlip2  26035  c1liplem1  26036  dvgt0lem1  26042  lhop1lem  26053  dvcnvrelem1  26057  dvcvx  26060  ftc2ditglem  26087  wilthlem2  27113  dchrval  27279  dchrelbas2  27282  noresle  27743  nosupcbv  27748  nosupno  27749  nosupdm  27750  nosupfv  27752  nosupres  27753  nosupbnd1lem1  27754  nosupbnd1lem3  27756  nosupbnd1lem5  27758  nosupbnd1  27760  nosupbnd2  27762  noinfcbv  27763  noinfno  27764  noinfdm  27765  noinffv  27767  noinfres  27768  noinfbnd1lem3  27771  noinfbnd1lem5  27773  noinfbnd1  27775  noinfbnd2  27777  noetalem1  27787  norecov  27981  norec2ov  27991  egrsubgr  29295  dfpth2  29750  pthdlem1  29787  eupthvdres  30255  eupth2lem3  30256  eupth2  30259  eucrct2eupth  30265  hhssablo  31283  hhssnvt  31285  hhsssh  31289  fressupp  32698  resf1o  32742  gsummpt2d  33053  gsumpart  33061  symgcom  33104  tocycval  33129  tocycfv  33130  tocycf  33138  tocyc01  33139  cycpm2tr  33140  cycpmconjslem1  33175  cycpmconjslem2  33176  nsgqusf1o  33445  qtophaus  33836  esumcvg  34088  eulerpartlemn  34384  sseqp1  34398  signsvtn0  34586  ftc2re  34614  reprsuc  34631  bnj1385  34847  bnj1326  35041  bnj1321  35042  bnj1442  35064  bnj1450  35065  bnj1463  35070  bnj1529  35085  f1resfz0f1d  35120  pfxwlk  35130  pthhashvtx  35134  cvmliftlem5  35295  cvmliftlem7  35297  cvmliftlem10  35300  cvmliftlem11  35301  cvmliftlem15  35304  cvmlift2lem11  35319  cvmlift2lem12  35320  satffunlem1lem1  35408  satffunlem2lem1  35410  eldm3  35762  funsseq  35769  finixpnum  37613  poimirlem3  37631  poimirlem4  37632  poimirlem9  37637  sdclem2  37750  prdsbnd2  37803  isdivrngo  37958  drngoi  37959  elrefsymrels2  38571  eleqvrels2  38594  dibffval  41143  hdmapffval  41829  hdmapfval  41830  eqresfnbd  42273  dvun  42394  eldiophb  42773  diophrw  42775  diophin  42788  tfsconcatrev  43366  ofoafg  43372  resisoeq45d  43438  rclexi  43633  rtrclex  43635  rtrclexi  43639  cnvrcl0  43643  dfrtrcl5  43647  dfrcl2  43692  fvmptiunrelexplb0da  43703  sblpnf  44334  fresin2  45182  limsupresuz  45723  limsupvaluz  45728  limsupvaluz2  45758  supcnvlimsup  45760  climrescn  45768  liminfresuz  45804  cncfuni  45906  dvresntr  45938  dvbdfbdioolem1  45948  itgiccshift  46000  itgperiod  46001  dirkercncflem2  46124  fourierdlem46  46172  fourierdlem48  46174  fourierdlem49  46175  fourierdlem58  46184  fourierdlem72  46198  fourierdlem74  46200  fourierdlem75  46201  fourierdlem81  46207  fourierdlem88  46214  fourierdlem89  46215  fourierdlem90  46216  fourierdlem91  46217  fourierdlem92  46218  fourierdlem103  46229  fourierdlem104  46230  fourierdlem112  46238  fouriersw  46251  voncmpl  46641  funcoressn  47059  funressnmo  47063  f1cof1blem  47091  funfocofob  47095  funressndmafv2rn  47240  f1oresf1orab  47306  isubgrgrim  47902  stgrfv  47925  gpgov  48006  rngcidALTV  48195  rhmsubcALTVlem3  48204  funcringcsetcALTV2lem5  48215  ringcidALTV  48229  funcringcsetclem5ALTV  48238  itcoval  48587  itcoval0mpt  48592  itcovalendof  48595  dfswapf2  48985  fucofvalg  49036  fucof1  49040  fucofvalne  49043  idfudiag1  49183  aacllem  49375