Theorem reseq2d 5700

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

Syntax hints:   → wi 4   = wceq 1508   ↾ cres 5413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2752

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2761  df-cleq 2773  df-clel 2848  df-nfc 2920  df-rab 3099  df-v 3419  df-in 3838  df-opab 4997  df-xp 5417  df-res 5423

This theorem is referenced by:  reseq12d  5701  resresdm  5934  relresfld  5970  f1orescnv  6464  fococnv2  6474  fvn0ssdmfun  6673  fnressn  6749  fnsnsplit  6779  oprssov  7139  curry1  7613  curry2  7616  dftpos2  7718  wrecseq123  7757  wfr3g  7762  wfrlem1  7763  wfrlem4  7767  wfrlem4OLD  7768  wfrlem14  7778  wfr2a  7782  dfrecs3  7819  tfrlem16  7839  tfr2ALT  7847  tfr3ALT  7848  sbthlem4  8432  mapunen  8488  hartogslem1  8807  axdc3lem2  9677  fseq1p1m1  12803  resunimafz0  13622  hashf1lem1  13632  relexp0g  14248  relexp0  14249  relexpsucnnr  14251  dfrtrcl2  14288  bpolylem  15268  setsval  16375  idfuval  17016  idfu2nd  17017  resf1st  17034  setcid  17216  catcisolem  17236  estrcid  17254  funcestrcsetclem5  17264  funcsetcestrclem5  17279  funcsetcestrclem7  17281  1stfval  17311  1stf2  17313  2ndfval  17314  2ndf2  17316  1stfcl  17317  2ndfcl  17318  curf2ndf  17367  hofcl  17379  isps  17682  cnvps  17692  isdir  17712  dirref  17715  tsrdir  17718  frmdval  17869  frmdplusg  17872  gsum2dlem2  18856  dprd2da  18926  dpjval  18940  ablfac1eulem  18956  ablfac1eu  18957  psrplusg  19887  opsrtoslem2  19990  mdetunilem3  20942  mdetunilem4  20943  mdetunilem9  20948  imacmp  21724  ptuncnv  22134  tgphaus  22443  tsmsres  22470  tsmsxplem1  22479  tsmsxplem2  22480  trust  22556  metreslem  22690  imasdsf1olem  22701  xmspropd  22801  mspropd  22802  imasf1oxms  22817  imasf1oms  22818  nmpropd2  22922  isngp2  22924  ngppropd  22964  tngngp2  22979  cphsscph  23572  cmspropd  23670  cmssmscld  23671  mbfres2  23964  limciun  24210  dvmptres3  24271  dvmptres2  24277  dvmptntr  24286  dvlipcn  24309  dvlip2  24310  c1liplem1  24311  dvgt0lem1  24317  lhop1lem  24328  dvcnvrelem1  24332  dvcvx  24335  ftc2ditglem  24360  wilthlem2  25363  dchrval  25527  dchrelbas2  25530  egrsubgr  26777  pthdlem1  27270  eupthvdres  27780  eupth2lem3  27781  eupth2  27784  eucrct2eupthOLD  27791  eucrct2eupth  27792  hhssablo  28834  hhssnvt  28836  hhsssh  28840  fnunres1  30137  resf1o  30242  tocycval  30472  tocycfv  30473  tocycf  30479  cycpm2tr  30480  gsummpt2d  30556  qtophaus  30776  esumcvg  31021  eulerpartlemn  31316  sseqp1  31331  signsvtn0  31518  signsvtn0OLD  31519  ftc2re  31549  reprsuc  31566  bnj1385  31784  bnj1326  31975  bnj1321  31976  bnj1442  31998  bnj1450  31999  bnj1463  32004  bnj1529  32019  cvmliftlem5  32161  cvmliftlem7  32163  cvmliftlem10  32166  cvmliftlem11  32167  cvmliftlem15  32170  cvmlift2lem11  32185  cvmlift2lem12  32186  eldm3  32557  funsseq  32571  frecseq123  32680  frr3g  32682  fpr3g  32683  frrlem1  32684  frrlem4  32687  frrlem12  32695  fpr2  32701  frr2  32706  noresle  32761  nosupno  32764  nosupdm  32765  nosupfv  32767  nosupres  32768  nosupbnd1lem1  32769  nosupbnd1lem3  32771  nosupbnd1lem5  32773  nosupbnd1  32775  nosupbnd2  32777  noeta  32783  finixpnum  34358  poimirlem3  34376  poimirlem4  34377  poimirlem9  34382  sdclem2  34499  prdsbnd2  34555  isdivrngo  34710  drngoi  34711  elrefsymrels2  35290  eleqvrels2  35312  dibffval  37761  hdmapffval  38447  hdmapfval  38448  eldiophb  38790  diophrw  38792  diophin  38806  rclexi  39379  rtrclex  39381  rtrclexi  39385  cnvrcl0  39389  dfrtrcl5  39393  dfrcl2  39423  fvmptiunrelexplb0da  39434  sblpnf  40099  fresin2  40889  limsupresuz  41450  limsupvaluz  41455  limsupvaluz2  41485  supcnvlimsup  41487  climrescn  41495  liminfresuz  41531  cncfuni  41634  dvresntr  41667  dvbdfbdioolem1  41678  itgiccshift  41730  itgperiod  41731  dirkercncflem2  41855  fourierdlem46  41903  fourierdlem48  41905  fourierdlem49  41906  fourierdlem58  41915  fourierdlem72  41929  fourierdlem74  41931  fourierdlem75  41932  fourierdlem81  41938  fourierdlem88  41945  fourierdlem89  41946  fourierdlem90  41947  fourierdlem91  41948  fourierdlem92  41949  fourierdlem103  41960  fourierdlem104  41961  fourierdlem112  41969  fouriersw  41982  voncmpl  42369  funcoressn  42717  funressnmo  42722  funressndmafv2rn  42863  f1oresf1orab  42929  isomgreqve  43393  idfusubc0  43535  idfusubc  43536  rngcval  43632  rnghmsubcsetclem1  43645  rngccat  43648  rngcid  43649  rngcidALTV  43661  rngcifuestrc  43667  funcrngcsetc  43668  funcrngcsetcALT  43669  ringcval  43678  rhmsubcsetclem1  43691  ringccat  43694  ringcid  43695  rhmsubcrngclem1  43697  rhmsubcrngc  43699  funcringcsetc  43705  funcringcsetcALTV2lem5  43710  ringcidALTV  43724  funcringcsetclem5ALTV  43733  rhmsubc  43760  rhmsubcALTVlem3  43776  aacllem  44304