Theorem reseq2d 5980

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

Syntax hints:   → wi 4   = wceq 1570   ↾ cres 5665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-in 3913  df-opab 5175  df-xp 5669  df-res 5675

This theorem is referenced by:  reseq12d  5981  imadifssranOLD  6205  resresdm  6236  relresfld  6279  fnunres1  6649  f1orescnv  6838  fococnv2  6849  fvn0ssdmfun  7071  fnressn  7157  fnsnsplit  7184  oprssov  7581  curry1  8100  curry2  8103  dftpos2  8240  frecseq123  8280  fpr3g  8283  frrlem1  8284  frrlem4  8287  frrlem12  8295  fpr2a  8300  wfr3g  8317  dfrecs3  8360  tfrlem16  8381  tfr2ALT  8389  tfr3ALT  8390  on2recsov  8655  sbthlem4  9079  mapunen  9135  hartogslem1  9505  frr3g  9729  frr2  9733  axdc3lem2  10436  fseq1p1m1  13628  resunimafz0  14484  hashf1lem1  14494  relexp0g  15061  relexp0  15062  relexpsucnnr  15064  dfrtrcl2  15101  bpolylem  16103  setsval  17228  idfuval  17934  idfu2nd  17935  resf1st  17952  idfusubc0  17957  idfusubc  17958  setcid  18144  catcisolem  18168  estrcid  18191  funcestrcsetclem5  18201  funcsetcestrclem5  18216  funcsetcestrclem7  18218  1stfval  18248  1stf2  18250  2ndfval  18251  2ndf2  18253  1stfcl  18254  2ndfcl  18255  curf2ndf  18304  hofcl  18316  isps  18625  cnvps  18635  isdir  18655  dirref  18658  tsrdir  18661  frmdval  18911  frmdplusg  18914  gsum2dlem2  20042  dprd2da  20115  dpjval  20129  ablfac1eulem  20145  ablfac1eu  20146  rngcval  20704  rnghmsubcsetclem1  20717  rngccat  20720  rngcid  20721  rngcifuestrc  20725  funcrngcsetc  20726  funcrngcsetcALT  20727  ringcval  20733  rhmsubcsetclem1  20746  ringccat  20749  ringcid  20750  rhmsubcrngclem1  20752  rhmsubcrngc  20754  funcringcsetc  20760  rhmsubc  20775  psrplusg  22068  opsrtoslem2  22188  mdetunilem3  22752  mdetunilem4  22753  mdetunilem9  22758  imacmp  23535  ptuncnv  23945  tgphaus  24255  tsmsres  24282  tsmsxplem1  24291  tsmsxplem2  24292  trust  24367  metreslem  24500  imasdsf1olem  24511  xmspropd  24611  mspropd  24612  imasf1oxms  24627  imasf1oms  24628  nmpropd2  24733  isngp2  24735  ngppropd  24775  tngngp2  24790  cphsscph  25391  cmspropd  25489  cmssmscld  25490  mbfres2  25785  limciun  26034  dvmptres3  26096  dvmptres2  26102  dvmptntr  26111  dvlipcn  26134  dvlip2  26135  c1liplem1  26136  dvgt0lem1  26142  lhop1lem  26153  dvcnvrelem1  26157  dvcvx  26160  ftc2ditglem  26185  wilthlem2  27211  dchrval  27376  dchrelbas2  27379  noresle  27839  nosupcbv  27844  nosupno  27845  nosupdm  27846  nosupfv  27848  nosupres  27849  nosupbnd1lem1  27850  nosupbnd1lem3  27852  nosupbnd1lem5  27854  nosupbnd1  27856  nosupbnd2  27858  noinfcbv  27859  noinfno  27860  noinfdm  27861  noinffv  27863  noinfres  27864  noinfbnd1lem3  27867  noinfbnd1lem5  27869  noinfbnd1  27871  noinfbnd2  27873  noetalem1  27883  norecov  28118  norec2ov  28128  egrsubgr  29605  dfpth2  30056  pthdlem1  30093  eupthvdres  30564  eupth2lem3  30565  eupth2  30568  eucrct2eupth  30574  hhssablo  31593  hhssnvt  31595  hhsssh  31599  fresunsn  32948  fressupp  33011  resf1o  33053  gsummpt2d  33347  gsumpart  33361  symgcom  33381  tocycval  33406  tocycfv  33407  tocycf  33415  tocyc01  33416  cycpm2tr  33417  cycpmconjslem1  33452  cycpmconjslem2  33453  nsgqusf1o  33703  extvval  33899  extvfval  33900  extvfvcl  33904  qtophaus  34204  esumcvg  34454  eulerpartlemn  34749  sseqp1  34763  signsvtn0  34935  ftc2re  34963  reprsuc  34980  bnj1385  35198  bnj1326  35392  bnj1321  35393  bnj1442  35415  bnj1450  35416  bnj1463  35421  bnj1529  35436  f1resfz0f1d  35583  pfxwlk  35594  pthhashvtx  35598  cvmliftlem5  35759  cvmliftlem7  35761  cvmliftlem10  35764  cvmliftlem11  35765  cvmliftlem15  35768  cvmlift2lem11  35783  cvmlift2lem12  35784  satffunlem1lem1  35872  satffunlem2lem1  35874  eldm3  36231  funsseq  36238  finixpnum  38234  poimirlem3  38252  poimirlem4  38253  poimirlem9  38258  sdclem2  38371  prdsbnd2  38424  isdivrngo  38579  drngoi  38580  elrefsymrels2  39280  eleqvrels2  39303  dibffval  41892  hdmapffval  42578  hdmapfval  42579  eqresfnbd  42981  dvun  43098  eldiophb  43468  diophrw  43470  diophin  43483  tfsconcatrev  44055  ofoafg  44061  resisoeq45d  44126  rclexi  44321  rtrclex  44323  rtrclexi  44327  cnvrcl0  44331  dfrtrcl5  44335  dfrcl2  44380  fvmptiunrelexplb0da  44391  sblpnf  45000  fresin2  45870  limsupresuz  46397  limsupvaluz  46402  limsupvaluz2  46432  supcnvlimsup  46434  climrescn  46442  liminfresuz  46478  cncfuni  46580  dvresntr  46612  dvbdfbdioolem1  46622  itgiccshift  46674  itgperiod  46675  dirkercncflem2  46798  fourierdlem46  46846  fourierdlem48  46848  fourierdlem49  46849  fourierdlem58  46858  fourierdlem72  46872  fourierdlem74  46874  fourierdlem75  46875  fourierdlem81  46881  fourierdlem88  46888  fourierdlem89  46889  fourierdlem90  46890  fourierdlem91  46891  fourierdlem92  46892  fourierdlem103  46903  fourierdlem104  46904  fourierdlem112  46912  fouriersw  46925  voncmpl  47315  funcoressn  47756  funressnmo  47760  f1cof1blem  47788  funfocofob  47792  funressndmafv2rn  47937  f1oresf1orab  48003  upgrimpths  48651  isubgrgrim  48671  stgrfv  48695  gpgov  48784  rngcidALTV  49016  rhmsubcALTVlem3  49025  funcringcsetcALTV2lem5  49036  ringcidALTV  49050  funcringcsetclem5ALTV  49059  itcoval  49418  itcoval0mpt  49423  itcovalendof  49426  idfu1sta  49856  idfu2nda  49858  imaidfu2  49866  idfullsubc  49916  dfswapf2  50016  oppc1stf  50043  oppc2ndf  50044  1stfpropd  50045  2ndfpropd  50046  fucofvalg  50073  fucof1  50077  fucofvalne  50080  opf2fval  50160  idfudiag1  50280  aacllem  50578