Theorem reseq2d 5938

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

Syntax hints:   → wi 4   = wceq 1547   ↾ cres 5627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-in 3897  df-opab 5142  df-xp 5631  df-res 5637

This theorem is referenced by:  reseq12d  5939  imadifssran  6109  resresdm  6191  relresfld  6234  fnunres1  6604  f1orescnv  6789  fococnv2  6800  fvn0ssdmfun  7022  fnressn  7108  fnsnsplit  7135  oprssov  7532  curry1  8050  curry2  8053  dftpos2  8190  frecseq123  8229  fpr3g  8232  frrlem1  8233  frrlem4  8236  frrlem12  8244  fpr2a  8249  wfr3g  8266  dfrecs3  8309  tfrlem16  8329  tfr2ALT  8337  tfr3ALT  8338  on2recsov  8601  sbthlem4  9025  mapunen  9081  hartogslem1  9454  frr3g  9678  frr2  9682  axdc3lem2  10371  fseq1p1m1  13550  resunimafz0  14405  hashf1lem1  14415  relexp0g  14982  relexp0  14983  relexpsucnnr  14985  dfrtrcl2  15022  bpolylem  16011  setsval  17135  idfuval  17841  idfu2nd  17842  resf1st  17859  idfusubc0  17864  idfusubc  17865  setcid  18051  catcisolem  18075  estrcid  18098  funcestrcsetclem5  18108  funcsetcestrclem5  18123  funcsetcestrclem7  18125  1stfval  18155  1stf2  18157  2ndfval  18158  2ndf2  18160  1stfcl  18161  2ndfcl  18162  curf2ndf  18211  hofcl  18223  isps  18532  cnvps  18542  isdir  18562  dirref  18565  tsrdir  18568  frmdval  18817  frmdplusg  18820  gsum2dlem2  19944  dprd2da  20017  dpjval  20031  ablfac1eulem  20047  ablfac1eu  20048  rngcval  20597  rnghmsubcsetclem1  20610  rngccat  20613  rngcid  20614  rngcifuestrc  20618  funcrngcsetc  20619  funcrngcsetcALT  20620  ringcval  20626  rhmsubcsetclem1  20639  ringccat  20642  ringcid  20643  rhmsubcrngclem1  20645  rhmsubcrngc  20647  funcringcsetc  20653  rhmsubc  20668  psrplusg  21919  opsrtoslem2  22039  mdetunilem3  22604  mdetunilem4  22605  mdetunilem9  22610  imacmp  23387  ptuncnv  23797  tgphaus  24107  tsmsres  24134  tsmsxplem1  24143  tsmsxplem2  24144  trust  24219  metreslem  24352  imasdsf1olem  24363  xmspropd  24463  mspropd  24464  imasf1oxms  24479  imasf1oms  24480  nmpropd2  24585  isngp2  24587  ngppropd  24627  tngngp2  24642  cphsscph  25243  cmspropd  25341  cmssmscld  25342  mbfres2  25637  limciun  25886  dvmptres3  25948  dvmptres2  25954  dvmptntr  25963  dvlipcn  25986  dvlip2  25987  c1liplem1  25988  dvgt0lem1  25994  lhop1lem  26005  dvcnvrelem1  26009  dvcvx  26012  ftc2ditglem  26037  wilthlem2  27057  dchrval  27222  dchrelbas2  27225  noresle  27686  nosupcbv  27691  nosupno  27692  nosupdm  27693  nosupfv  27695  nosupres  27696  nosupbnd1lem1  27697  nosupbnd1lem3  27699  nosupbnd1lem5  27701  nosupbnd1  27703  nosupbnd2  27705  noinfcbv  27706  noinfno  27707  noinfdm  27708  noinffv  27710  noinfres  27711  noinfbnd1lem3  27714  noinfbnd1lem5  27716  noinfbnd1  27718  noinfbnd2  27720  noetalem1  27730  norecov  27964  norec2ov  27974  egrsubgr  29371  dfpth2  29822  pthdlem1  29859  eupthvdres  30330  eupth2lem3  30331  eupth2  30334  eucrct2eupth  30340  hhssablo  31359  hhssnvt  31361  hhsssh  31365  fresunsn  32724  fressupp  32787  resf1o  32829  gsummpt2d  33137  gsumpart  33151  symgcom  33171  tocycval  33196  tocycfv  33197  tocycf  33205  tocyc01  33206  cycpm2tr  33207  cycpmconjslem1  33242  cycpmconjslem2  33243  nsgqusf1o  33506  extvval  33722  extvfval  33723  extvfvcl  33727  qtophaus  34027  esumcvg  34277  eulerpartlemn  34572  sseqp1  34586  signsvtn0  34761  ftc2re  34789  reprsuc  34806  bnj1385  35021  bnj1326  35215  bnj1321  35216  bnj1442  35238  bnj1450  35239  bnj1463  35244  bnj1529  35259  f1resfz0f1d  35349  pfxwlk  35359  pthhashvtx  35363  cvmliftlem5  35524  cvmliftlem7  35526  cvmliftlem10  35529  cvmliftlem11  35530  cvmliftlem15  35533  cvmlift2lem11  35548  cvmlift2lem12  35549  satffunlem1lem1  35637  satffunlem2lem1  35639  eldm3  35996  funsseq  36003  finixpnum  37979  poimirlem3  37997  poimirlem4  37998  poimirlem9  38003  sdclem2  38116  prdsbnd2  38169  isdivrngo  38324  drngoi  38325  elrefsymrels2  39027  eleqvrels2  39050  dibffval  41639  hdmapffval  42325  hdmapfval  42326  eqresfnbd  42726  dvun  42843  eldiophb  43213  diophrw  43215  diophin  43228  tfsconcatrev  43800  ofoafg  43806  resisoeq45d  43871  rclexi  44066  rtrclex  44068  rtrclexi  44072  cnvrcl0  44076  dfrtrcl5  44080  dfrcl2  44125  fvmptiunrelexplb0da  44136  sblpnf  44761  fresin2  45626  limsupresuz  46153  limsupvaluz  46158  limsupvaluz2  46188  supcnvlimsup  46190  climrescn  46198  liminfresuz  46234  cncfuni  46336  dvresntr  46368  dvbdfbdioolem1  46378  itgiccshift  46430  itgperiod  46431  dirkercncflem2  46554  fourierdlem46  46602  fourierdlem48  46604  fourierdlem49  46605  fourierdlem58  46614  fourierdlem72  46628  fourierdlem74  46630  fourierdlem75  46631  fourierdlem81  46637  fourierdlem88  46644  fourierdlem89  46645  fourierdlem90  46646  fourierdlem91  46647  fourierdlem92  46648  fourierdlem103  46659  fourierdlem104  46660  fourierdlem112  46668  fouriersw  46681  voncmpl  47071  funcoressn  47512  funressnmo  47516  f1cof1blem  47544  funfocofob  47548  funressndmafv2rn  47693  f1oresf1orab  47759  upgrimpths  48407  isubgrgrim  48427  stgrfv  48451  gpgov  48540  rngcidALTV  48772  rhmsubcALTVlem3  48781  funcringcsetcALTV2lem5  48792  ringcidALTV  48806  funcringcsetclem5ALTV  48815  itcoval  49159  itcoval0mpt  49164  itcovalendof  49167  idfu1sta  49598  idfu2nda  49600  imaidfu2  49608  idfullsubc  49658  dfswapf2  49758  oppc1stf  49785  oppc2ndf  49786  1stfpropd  49787  2ndfpropd  49788  fucofvalg  49815  fucof1  49819  fucofvalne  49822  opf2fval  49902  idfudiag1  50022  aacllem  50298