Theorem reseq2d 5928

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

Syntax hints:   → wi 4   = wceq 1541   ↾ cres 5618

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 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-in 3909  df-opab 5154  df-xp 5622  df-res 5628

This theorem is referenced by:  reseq12d  5929  imadifssran  6098  resresdm  6180  relresfld  6223  fnunres1  6593  f1orescnv  6778  fococnv2  6789  fvn0ssdmfun  7007  fnressn  7091  fnsnsplit  7118  oprssov  7515  curry1  8034  curry2  8037  dftpos2  8173  frecseq123  8212  fpr3g  8215  frrlem1  8216  frrlem4  8219  frrlem12  8227  fpr2a  8232  wfr3g  8249  dfrecs3  8292  tfrlem16  8312  tfr2ALT  8320  tfr3ALT  8321  on2recsov  8583  sbthlem4  9003  mapunen  9059  hartogslem1  9428  frr3g  9646  frr2  9650  axdc3lem2  10339  fseq1p1m1  13495  resunimafz0  14349  hashf1lem1  14359  relexp0g  14926  relexp0  14927  relexpsucnnr  14929  dfrtrcl2  14966  bpolylem  15952  setsval  17075  idfuval  17780  idfu2nd  17781  resf1st  17798  idfusubc0  17803  idfusubc  17804  setcid  17990  catcisolem  18014  estrcid  18037  funcestrcsetclem5  18047  funcsetcestrclem5  18062  funcsetcestrclem7  18064  1stfval  18094  1stf2  18096  2ndfval  18097  2ndf2  18099  1stfcl  18100  2ndfcl  18101  curf2ndf  18150  hofcl  18162  isps  18471  cnvps  18481  isdir  18501  dirref  18504  tsrdir  18507  frmdval  18756  frmdplusg  18759  gsum2dlem2  19881  dprd2da  19954  dpjval  19968  ablfac1eulem  19984  ablfac1eu  19985  rngcval  20531  rnghmsubcsetclem1  20544  rngccat  20547  rngcid  20548  rngcifuestrc  20552  funcrngcsetc  20553  funcrngcsetcALT  20554  ringcval  20560  rhmsubcsetclem1  20573  ringccat  20576  ringcid  20577  rhmsubcrngclem1  20579  rhmsubcrngc  20581  funcringcsetc  20587  rhmsubc  20602  psrplusg  21871  opsrtoslem2  21989  mdetunilem3  22527  mdetunilem4  22528  mdetunilem9  22533  imacmp  23310  ptuncnv  23720  tgphaus  24030  tsmsres  24057  tsmsxplem1  24066  tsmsxplem2  24067  trust  24142  metreslem  24275  imasdsf1olem  24286  xmspropd  24386  mspropd  24387  imasf1oxms  24402  imasf1oms  24403  nmpropd2  24508  isngp2  24510  ngppropd  24550  tngngp2  24565  cphsscph  25176  cmspropd  25274  cmssmscld  25275  mbfres2  25571  limciun  25820  dvmptres3  25885  dvmptres2  25891  dvmptntr  25900  dvlipcn  25924  dvlip2  25925  c1liplem1  25926  dvgt0lem1  25932  lhop1lem  25943  dvcnvrelem1  25947  dvcvx  25950  ftc2ditglem  25977  wilthlem2  27004  dchrval  27170  dchrelbas2  27173  noresle  27634  nosupcbv  27639  nosupno  27640  nosupdm  27641  nosupfv  27643  nosupres  27644  nosupbnd1lem1  27645  nosupbnd1lem3  27647  nosupbnd1lem5  27649  nosupbnd1  27651  nosupbnd2  27653  noinfcbv  27654  noinfno  27655  noinfdm  27656  noinffv  27658  noinfres  27659  noinfbnd1lem3  27662  noinfbnd1lem5  27664  noinfbnd1  27666  noinfbnd2  27668  noetalem1  27678  norecov  27888  norec2ov  27898  egrsubgr  29253  dfpth2  29705  pthdlem1  29742  eupthvdres  30210  eupth2lem3  30211  eupth2  30214  eucrct2eupth  30220  hhssablo  31238  hhssnvt  31240  hhsssh  31244  fressupp  32664  resf1o  32708  gsummpt2d  33024  gsumpart  33032  symgcom  33047  tocycval  33072  tocycfv  33073  tocycf  33081  tocyc01  33082  cycpm2tr  33083  cycpmconjslem1  33118  cycpmconjslem2  33119  nsgqusf1o  33376  qtophaus  33844  esumcvg  34094  eulerpartlemn  34389  sseqp1  34403  signsvtn0  34578  ftc2re  34606  reprsuc  34623  bnj1385  34839  bnj1326  35033  bnj1321  35034  bnj1442  35056  bnj1450  35057  bnj1463  35062  bnj1529  35077  f1resfz0f1d  35146  pfxwlk  35156  pthhashvtx  35160  cvmliftlem5  35321  cvmliftlem7  35323  cvmliftlem10  35326  cvmliftlem11  35327  cvmliftlem15  35330  cvmlift2lem11  35345  cvmlift2lem12  35346  satffunlem1lem1  35434  satffunlem2lem1  35436  eldm3  35793  funsseq  35800  finixpnum  37644  poimirlem3  37662  poimirlem4  37663  poimirlem9  37668  sdclem2  37781  prdsbnd2  37834  isdivrngo  37989  drngoi  37990  elrefsymrels2  38605  eleqvrels2  38628  dibffval  41178  hdmapffval  41864  hdmapfval  41865  eqresfnbd  42264  dvun  42391  eldiophb  42789  diophrw  42791  diophin  42804  tfsconcatrev  43380  ofoafg  43386  resisoeq45d  43452  rclexi  43647  rtrclex  43649  rtrclexi  43653  cnvrcl0  43657  dfrtrcl5  43661  dfrcl2  43706  fvmptiunrelexplb0da  43717  sblpnf  44342  fresin2  45208  limsupresuz  45740  limsupvaluz  45745  limsupvaluz2  45775  supcnvlimsup  45777  climrescn  45785  liminfresuz  45821  cncfuni  45923  dvresntr  45955  dvbdfbdioolem1  45965  itgiccshift  46017  itgperiod  46018  dirkercncflem2  46141  fourierdlem46  46189  fourierdlem48  46191  fourierdlem49  46192  fourierdlem58  46201  fourierdlem72  46215  fourierdlem74  46217  fourierdlem75  46218  fourierdlem81  46224  fourierdlem88  46231  fourierdlem89  46232  fourierdlem90  46233  fourierdlem91  46234  fourierdlem92  46235  fourierdlem103  46246  fourierdlem104  46247  fourierdlem112  46255  fouriersw  46268  voncmpl  46658  funcoressn  47072  funressnmo  47076  f1cof1blem  47104  funfocofob  47108  funressndmafv2rn  47253  f1oresf1orab  47319  upgrimpths  47939  isubgrgrim  47959  stgrfv  47983  gpgov  48072  rngcidALTV  48304  rhmsubcALTVlem3  48313  funcringcsetcALTV2lem5  48324  ringcidALTV  48338  funcringcsetclem5ALTV  48347  itcoval  48692  itcoval0mpt  48697  itcovalendof  48700  idfu1sta  49132  idfu2nda  49134  imaidfu2  49142  idfullsubc  49192  dfswapf2  49292  oppc1stf  49319  oppc2ndf  49320  1stfpropd  49321  2ndfpropd  49322  fucofvalg  49349  fucof1  49353  fucofvalne  49356  opf2fval  49436  idfudiag1  49556  aacllem  49832