Theorem reseq2d 5981

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-in 3955  df-opab 5211  df-xp 5682  df-res 5688

This theorem is referenced by:  reseq12d  5982  resresdm  6232  relresfld  6275  fnunres1  6661  f1orescnv  6848  fococnv2  6859  fvn0ssdmfun  7076  fnressn  7158  fnsnsplit  7184  oprssov  7580  curry1  8095  curry2  8098  dftpos2  8234  frecseq123  8273  fpr3g  8276  frrlem1  8277  frrlem4  8280  frrlem12  8288  fpr2a  8293  wrecseq123OLD  8306  wfr3g  8313  wfrlem1OLD  8314  wfrlem4OLD  8318  wfrlem14OLD  8328  wfr2aOLD  8332  dfrecs3  8378  dfrecs3OLD  8379  tfrlem16  8399  tfr2ALT  8407  tfr3ALT  8408  on2recsov  8673  sbthlem4  9092  mapunen  9152  hartogslem1  9543  frr3g  9757  frr2  9761  axdc3lem2  10452  fseq1p1m1  13582  resunimafz0  14411  hashf1lem1  14422  hashf1lem1OLD  14423  relexp0g  14976  relexp0  14977  relexpsucnnr  14979  dfrtrcl2  15016  bpolylem  15999  setsval  17107  idfuval  17833  idfu2nd  17834  resf1st  17851  idfusubc0  17856  idfusubc  17857  setcid  18046  catcisolem  18070  estrcid  18095  funcestrcsetclem5  18106  funcsetcestrclem5  18121  funcsetcestrclem7  18123  1stfval  18153  1stf2  18155  2ndfval  18156  2ndf2  18158  1stfcl  18159  2ndfcl  18160  curf2ndf  18210  hofcl  18222  isps  18531  cnvps  18541  isdir  18561  dirref  18564  tsrdir  18567  frmdval  18774  frmdplusg  18777  gsum2dlem2  19887  dprd2da  19960  dpjval  19974  ablfac1eulem  19990  ablfac1eu  19991  rngcval  20510  rnghmsubcsetclem1  20523  rngccat  20526  rngcid  20527  rngcifuestrc  20531  funcrngcsetc  20532  funcrngcsetcALT  20533  ringcval  20539  rhmsubcsetclem1  20552  ringccat  20555  ringcid  20556  rhmsubcrngclem1  20558  rhmsubcrngc  20560  funcringcsetc  20566  rhmsubc  20581  psrplusg  21810  opsrtoslem2  21928  mdetunilem3  22436  mdetunilem4  22437  mdetunilem9  22442  imacmp  23221  ptuncnv  23631  tgphaus  23941  tsmsres  23968  tsmsxplem1  23977  tsmsxplem2  23978  trust  24054  metreslem  24188  imasdsf1olem  24199  xmspropd  24299  mspropd  24300  imasf1oxms  24318  imasf1oms  24319  nmpropd2  24424  isngp2  24426  ngppropd  24466  tngngp2  24489  cphsscph  25099  cmspropd  25197  cmssmscld  25198  mbfres2  25494  limciun  25743  dvmptres3  25808  dvmptres2  25814  dvmptntr  25823  dvlipcn  25847  dvlip2  25848  c1liplem1  25849  dvgt0lem1  25855  lhop1lem  25866  dvcnvrelem1  25870  dvcvx  25873  ftc2ditglem  25900  wilthlem2  26914  dchrval  27080  dchrelbas2  27083  noresle  27543  nosupcbv  27548  nosupno  27549  nosupdm  27550  nosupfv  27552  nosupres  27553  nosupbnd1lem1  27554  nosupbnd1lem3  27556  nosupbnd1lem5  27558  nosupbnd1  27560  nosupbnd2  27562  noinfcbv  27563  noinfno  27564  noinfdm  27565  noinffv  27567  noinfres  27568  noinfbnd1lem3  27571  noinfbnd1lem5  27573  noinfbnd1  27575  noinfbnd2  27577  noetalem1  27587  norecov  27777  norec2ov  27787  egrsubgr  28967  pthdlem1  29456  eupthvdres  29921  eupth2lem3  29922  eupth2  29925  eucrct2eupth  29931  hhssablo  30949  hhssnvt  30951  hhsssh  30955  fressupp  32343  resf1o  32388  gsummpt2d  32637  gsumpart  32643  symgcom  32680  tocycval  32703  tocycfv  32704  tocycf  32712  tocyc01  32713  cycpm2tr  32714  cycpmconjslem1  32749  cycpmconjslem2  32750  nsgqusf1o  32967  qtophaus  33280  esumcvg  33548  eulerpartlemn  33844  sseqp1  33858  signsvtn0  34045  ftc2re  34074  reprsuc  34091  bnj1385  34307  bnj1326  34501  bnj1321  34502  bnj1442  34524  bnj1450  34525  bnj1463  34530  bnj1529  34545  f1resfz0f1d  34567  pfxwlk  34578  pthhashvtx  34582  cvmliftlem5  34744  cvmliftlem7  34746  cvmliftlem10  34749  cvmliftlem11  34750  cvmliftlem15  34753  cvmlift2lem11  34768  cvmlift2lem12  34769  satffunlem1lem1  34857  satffunlem2lem1  34859  eldm3  35201  funsseq  35209  finixpnum  36937  poimirlem3  36955  poimirlem4  36956  poimirlem9  36961  sdclem2  37074  prdsbnd2  37127  isdivrngo  37282  drngoi  37283  elrefsymrels2  37903  eleqvrels2  37926  dibffval  40475  hdmapffval  41161  hdmapfval  41162  eqresfnbd  41521  eldiophb  41958  diophrw  41960  diophin  41973  tfsconcatrev  42561  ofoafg  42567  resisoeq45d  42634  rclexi  42829  rtrclex  42831  rtrclexi  42835  cnvrcl0  42839  dfrtrcl5  42843  dfrcl2  42888  fvmptiunrelexplb0da  42899  sblpnf  43532  fresin2  44330  limsupresuz  44878  limsupvaluz  44883  limsupvaluz2  44913  supcnvlimsup  44915  climrescn  44923  liminfresuz  44959  cncfuni  45061  dvresntr  45093  dvbdfbdioolem1  45103  itgiccshift  45155  itgperiod  45156  dirkercncflem2  45279  fourierdlem46  45327  fourierdlem48  45329  fourierdlem49  45330  fourierdlem58  45339  fourierdlem72  45353  fourierdlem74  45355  fourierdlem75  45356  fourierdlem81  45362  fourierdlem88  45369  fourierdlem89  45370  fourierdlem90  45371  fourierdlem91  45372  fourierdlem92  45373  fourierdlem103  45384  fourierdlem104  45385  fourierdlem112  45393  fouriersw  45406  voncmpl  45796  funcoressn  46211  funressnmo  46215  f1cof1blem  46243  funfocofob  46245  funressndmafv2rn  46390  f1oresf1orab  46456  isomgreqve  46952  rngcidALTV  47111  rhmsubcALTVlem3  47120  funcringcsetcALTV2lem5  47131  ringcidALTV  47145  funcringcsetclem5ALTV  47154  itcoval  47509  itcoval0mpt  47514  itcovalendof  47517  aacllem  48010