Theorem reseq2d 5848

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

Syntax hints:   → wi 4   = wceq 1533   ↾ cres 5552

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-rab 3147  df-in 3943  df-opab 5122  df-xp 5556  df-res 5562

This theorem is referenced by:  reseq12d  5849  resresdm  6085  relresfld  6122  f1orescnv  6625  fococnv2  6635  fvn0ssdmfun  6837  fnressn  6915  fnsnsplit  6941  oprssov  7311  curry1  7793  curry2  7796  dftpos2  7903  wrecseq123  7942  wfr3g  7947  wfrlem1  7948  wfrlem4  7952  wfrlem14  7962  wfr2a  7966  dfrecs3  8003  tfrlem16  8023  tfr2ALT  8031  tfr3ALT  8032  sbthlem4  8624  mapunen  8680  hartogslem1  9000  axdc3lem2  9867  fseq1p1m1  12975  resunimafz0  13797  hashf1lem1  13807  relexp0g  14375  relexp0  14376  relexpsucnnr  14378  dfrtrcl2  14415  bpolylem  15396  setsval  16507  idfuval  17140  idfu2nd  17141  resf1st  17158  setcid  17340  catcisolem  17360  estrcid  17378  funcestrcsetclem5  17388  funcsetcestrclem5  17403  funcsetcestrclem7  17405  1stfval  17435  1stf2  17437  2ndfval  17438  2ndf2  17440  1stfcl  17441  2ndfcl  17442  curf2ndf  17491  hofcl  17503  isps  17806  cnvps  17816  isdir  17836  dirref  17839  tsrdir  17842  frmdval  18010  frmdplusg  18013  gsum2dlem2  19085  dprd2da  19158  dpjval  19172  ablfac1eulem  19188  ablfac1eu  19189  psrplusg  20155  opsrtoslem2  20259  mdetunilem3  21217  mdetunilem4  21218  mdetunilem9  21223  imacmp  21999  ptuncnv  22409  tgphaus  22719  tsmsres  22746  tsmsxplem1  22755  tsmsxplem2  22756  trust  22832  metreslem  22966  imasdsf1olem  22977  xmspropd  23077  mspropd  23078  imasf1oxms  23093  imasf1oms  23094  nmpropd2  23198  isngp2  23200  ngppropd  23240  tngngp2  23255  cphsscph  23848  cmspropd  23946  cmssmscld  23947  mbfres2  24240  limciun  24486  dvmptres3  24547  dvmptres2  24553  dvmptntr  24562  dvlipcn  24585  dvlip2  24586  c1liplem1  24587  dvgt0lem1  24593  lhop1lem  24604  dvcnvrelem1  24608  dvcvx  24611  ftc2ditglem  24636  wilthlem2  25640  dchrval  25804  dchrelbas2  25807  egrsubgr  27053  pthdlem1  27541  eupthvdres  28008  eupth2lem3  28009  eupth2  28012  eucrct2eupth  28018  hhssablo  29034  hhssnvt  29036  hhsssh  29040  fnunres1  30350  resf1o  30460  gsummpt2d  30682  symgcom  30722  tocycval  30745  tocycfv  30746  tocycf  30754  tocyc01  30755  cycpm2tr  30756  cycpmconjslem1  30791  cycpmconjslem2  30792  qtophaus  31095  esumcvg  31340  eulerpartlemn  31634  sseqp1  31648  signsvtn0  31835  ftc2re  31864  reprsuc  31881  bnj1385  32099  bnj1326  32293  bnj1321  32294  bnj1442  32316  bnj1450  32317  bnj1463  32322  bnj1529  32337  f1resfz0f1d  32356  pfxwlk  32365  pthhashvtx  32369  cvmliftlem5  32531  cvmliftlem7  32533  cvmliftlem10  32536  cvmliftlem11  32537  cvmliftlem15  32540  cvmlift2lem11  32555  cvmlift2lem12  32556  satffunlem1lem1  32644  satffunlem2lem1  32646  eldm3  32992  funsseq  33006  frecseq123  33114  frr3g  33116  fpr3g  33117  frrlem1  33118  frrlem4  33121  frrlem12  33129  fpr2  33135  frr2  33140  noresle  33195  nosupno  33198  nosupdm  33199  nosupfv  33201  nosupres  33202  nosupbnd1lem1  33203  nosupbnd1lem3  33205  nosupbnd1lem5  33207  nosupbnd1  33209  nosupbnd2  33211  noeta  33217  finixpnum  34871  poimirlem3  34889  poimirlem4  34890  poimirlem9  34895  sdclem2  35011  prdsbnd2  35067  isdivrngo  35222  drngoi  35223  elrefsymrels2  35799  eleqvrels2  35821  dibffval  38270  hdmapffval  38956  hdmapfval  38957  eldiophb  39347  diophrw  39349  diophin  39362  rclexi  39968  rtrclex  39970  rtrclexi  39974  cnvrcl0  39978  dfrtrcl5  39982  dfrcl2  40012  fvmptiunrelexplb0da  40023  sblpnf  40635  fresin2  41420  limsupresuz  41976  limsupvaluz  41981  limsupvaluz2  42011  supcnvlimsup  42013  climrescn  42021  liminfresuz  42057  cncfuni  42161  dvresntr  42194  dvbdfbdioolem1  42205  itgiccshift  42257  itgperiod  42258  dirkercncflem2  42382  fourierdlem46  42430  fourierdlem48  42432  fourierdlem49  42433  fourierdlem58  42442  fourierdlem72  42456  fourierdlem74  42458  fourierdlem75  42459  fourierdlem81  42465  fourierdlem88  42472  fourierdlem89  42473  fourierdlem90  42474  fourierdlem91  42475  fourierdlem92  42476  fourierdlem103  42487  fourierdlem104  42488  fourierdlem112  42496  fouriersw  42509  voncmpl  42896  funcoressn  43270  funressnmo  43274  funressndmafv2rn  43415  f1oresf1orab  43481  isomgreqve  43983  idfusubc0  44129  idfusubc  44130  rngcval  44226  rnghmsubcsetclem1  44239  rngccat  44242  rngcid  44243  rngcidALTV  44255  rngcifuestrc  44261  funcrngcsetc  44262  funcrngcsetcALT  44263  ringcval  44272  rhmsubcsetclem1  44285  ringccat  44288  ringcid  44289  rhmsubcrngclem1  44291  rhmsubcrngc  44293  funcringcsetc  44299  funcringcsetcALTV2lem5  44304  ringcidALTV  44318  funcringcsetclem5ALTV  44327  rhmsubc  44354  rhmsubcALTVlem3  44370  aacllem  44895