Theorem reseq2d 6009

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

Syntax hints:   → wi 4   = wceq 1537   ↾ cres 5702

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-in 3983  df-opab 5229  df-xp 5706  df-res 5712

This theorem is referenced by:  reseq12d  6010  resresdm  6264  relresfld  6307  fnunres1  6691  f1orescnv  6877  fococnv2  6888  fvn0ssdmfun  7108  fnressn  7192  fnsnsplit  7218  oprssov  7619  curry1  8145  curry2  8148  dftpos2  8284  frecseq123  8323  fpr3g  8326  frrlem1  8327  frrlem4  8330  frrlem12  8338  fpr2a  8343  wrecseq123OLD  8356  wfr3g  8363  wfrlem1OLD  8364  wfrlem4OLD  8368  wfrlem14OLD  8378  wfr2aOLD  8382  dfrecs3  8428  dfrecs3OLD  8429  tfrlem16  8449  tfr2ALT  8457  tfr3ALT  8458  on2recsov  8724  sbthlem4  9152  mapunen  9212  hartogslem1  9611  frr3g  9825  frr2  9829  axdc3lem2  10520  fseq1p1m1  13658  resunimafz0  14494  hashf1lem1  14504  relexp0g  15071  relexp0  15072  relexpsucnnr  15074  dfrtrcl2  15111  bpolylem  16096  setsval  17214  idfuval  17940  idfu2nd  17941  resf1st  17958  idfusubc0  17963  idfusubc  17964  setcid  18153  catcisolem  18177  estrcid  18202  funcestrcsetclem5  18213  funcsetcestrclem5  18228  funcsetcestrclem7  18230  1stfval  18260  1stf2  18262  2ndfval  18263  2ndf2  18265  1stfcl  18266  2ndfcl  18267  curf2ndf  18317  hofcl  18329  isps  18638  cnvps  18648  isdir  18668  dirref  18671  tsrdir  18674  frmdval  18886  frmdplusg  18889  gsum2dlem2  20013  dprd2da  20086  dpjval  20100  ablfac1eulem  20116  ablfac1eu  20117  rngcval  20640  rnghmsubcsetclem1  20653  rngccat  20656  rngcid  20657  rngcifuestrc  20661  funcrngcsetc  20662  funcrngcsetcALT  20663  ringcval  20669  rhmsubcsetclem1  20682  ringccat  20685  ringcid  20686  rhmsubcrngclem1  20688  rhmsubcrngc  20690  funcringcsetc  20696  rhmsubc  20711  psrplusg  21979  opsrtoslem2  22103  mdetunilem3  22641  mdetunilem4  22642  mdetunilem9  22647  imacmp  23426  ptuncnv  23836  tgphaus  24146  tsmsres  24173  tsmsxplem1  24182  tsmsxplem2  24183  trust  24259  metreslem  24393  imasdsf1olem  24404  xmspropd  24504  mspropd  24505  imasf1oxms  24523  imasf1oms  24524  nmpropd2  24629  isngp2  24631  ngppropd  24671  tngngp2  24694  cphsscph  25304  cmspropd  25402  cmssmscld  25403  mbfres2  25699  limciun  25949  dvmptres3  26014  dvmptres2  26020  dvmptntr  26029  dvlipcn  26053  dvlip2  26054  c1liplem1  26055  dvgt0lem1  26061  lhop1lem  26072  dvcnvrelem1  26076  dvcvx  26079  ftc2ditglem  26106  wilthlem2  27130  dchrval  27296  dchrelbas2  27299  noresle  27760  nosupcbv  27765  nosupno  27766  nosupdm  27767  nosupfv  27769  nosupres  27770  nosupbnd1lem1  27771  nosupbnd1lem3  27773  nosupbnd1lem5  27775  nosupbnd1  27777  nosupbnd2  27779  noinfcbv  27780  noinfno  27781  noinfdm  27782  noinffv  27784  noinfres  27785  noinfbnd1lem3  27788  noinfbnd1lem5  27790  noinfbnd1  27792  noinfbnd2  27794  noetalem1  27804  norecov  27998  norec2ov  28008  egrsubgr  29312  pthdlem1  29802  eupthvdres  30267  eupth2lem3  30268  eupth2  30271  eucrct2eupth  30277  hhssablo  31295  hhssnvt  31297  hhsssh  31301  fressupp  32700  resf1o  32744  gsummpt2d  33032  gsumpart  33038  symgcom  33076  tocycval  33101  tocycfv  33102  tocycf  33110  tocyc01  33111  cycpm2tr  33112  cycpmconjslem1  33147  cycpmconjslem2  33148  nsgqusf1o  33409  qtophaus  33782  esumcvg  34050  eulerpartlemn  34346  sseqp1  34360  signsvtn0  34547  ftc2re  34575  reprsuc  34592  bnj1385  34808  bnj1326  35002  bnj1321  35003  bnj1442  35025  bnj1450  35026  bnj1463  35031  bnj1529  35046  f1resfz0f1d  35081  pfxwlk  35091  pthhashvtx  35095  cvmliftlem5  35257  cvmliftlem7  35259  cvmliftlem10  35262  cvmliftlem11  35263  cvmliftlem15  35266  cvmlift2lem11  35281  cvmlift2lem12  35282  satffunlem1lem1  35370  satffunlem2lem1  35372  eldm3  35723  funsseq  35731  finixpnum  37565  poimirlem3  37583  poimirlem4  37584  poimirlem9  37589  sdclem2  37702  prdsbnd2  37755  isdivrngo  37910  drngoi  37911  elrefsymrels2  38525  eleqvrels2  38548  dibffval  41097  hdmapffval  41783  hdmapfval  41784  eqresfnbd  42227  eldiophb  42713  diophrw  42715  diophin  42728  tfsconcatrev  43310  ofoafg  43316  resisoeq45d  43382  rclexi  43577  rtrclex  43579  rtrclexi  43583  cnvrcl0  43587  dfrtrcl5  43591  dfrcl2  43636  fvmptiunrelexplb0da  43647  sblpnf  44279  fresin2  45079  limsupresuz  45624  limsupvaluz  45629  limsupvaluz2  45659  supcnvlimsup  45661  climrescn  45669  liminfresuz  45705  cncfuni  45807  dvresntr  45839  dvbdfbdioolem1  45849  itgiccshift  45901  itgperiod  45902  dirkercncflem2  46025  fourierdlem46  46073  fourierdlem48  46075  fourierdlem49  46076  fourierdlem58  46085  fourierdlem72  46099  fourierdlem74  46101  fourierdlem75  46102  fourierdlem81  46108  fourierdlem88  46115  fourierdlem89  46116  fourierdlem90  46117  fourierdlem91  46118  fourierdlem92  46119  fourierdlem103  46130  fourierdlem104  46131  fourierdlem112  46139  fouriersw  46152  voncmpl  46542  funcoressn  46957  funressnmo  46961  f1cof1blem  46989  funfocofob  46993  funressndmafv2rn  47138  f1oresf1orab  47204  isubgrgrim  47781  rngcidALTV  47997  rhmsubcALTVlem3  48006  funcringcsetcALTV2lem5  48017  ringcidALTV  48031  funcringcsetclem5ALTV  48040  itcoval  48395  itcoval0mpt  48400  itcovalendof  48403  aacllem  48895