Theorem reseq2d 5969

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ↾ cres 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-in 4091  df-opab 5167  df-xp 5656  df-res 5662

This theorem is used by:  reseq12d  5970  imadifssranOLDOLD  6203  resresdm  6234  relresfld  6278  relresfldOLD  6279  fnunres1  6651  f1orescnv  6840  fococnv2  6851  fvn0ssdmfun  7074  fnressn  7162  fnsnsplit  7189  oprssov  7590  curry1  8117  curry2  8120  dftpos2  8263  frecseq123  8303  fpr3g  8306  frrlem1  8307  frrlem4  8310  frrlem12  8318  fpr2a  8323  wfr3g  8340  dfrecs3  8383  tfrlem16  8404  tfr2ALT  8412  tfr3ALT  8413  on2recsov  8680  sbthlem4  9112  mapunen  9168  hartogslem1  9539  frr3g  9763  frr2  9767  axdc3lem2  10532  fseq1p1m1  13735  f1resfz0f1d  13930  resunimafz0  14593  hashf1lem1  14603  relexp0g  15180  relexp0  15181  relexpsucnnr  15183  dfrtrcl2  15220  bpolylem  16219  setsval  17350  idfuval  18056  idfu2nd  18057  resf1st  18074  idfusubc0  18079  idfusubc  18080  setcid  18266  catcisolem  18290  estrcid  18313  funcestrcsetclem5  18323  funcsetcestrclem5  18338  funcsetcestrclem7  18340  1stfval  18370  1stf2  18372  2ndfval  18373  2ndf2  18375  1stfcl  18376  2ndfcl  18377  curf2ndf  18426  hofcl  18438  isps  18747  cnvps  18757  isdir  18777  dirref  18780  tsrdir  18783  frmdval  19052  frmdplusg  19055  gsum2dlem2  20190  dprd2da  20263  dpjval  20277  ablfac1eulem  20293  ablfac1eu  20294  rngcval  20875  rnghmsubcsetclem1  20888  rngccat  20891  rngcid  20892  rngcifuestrc  20896  funcrngcsetc  20897  funcrngcsetcALT  20898  ringcval  20904  rhmsubcsetclem1  20917  ringccat  20920  ringcid  20921  rhmsubcrngclem1  20923  rhmsubcrngc  20925  funcringcsetc  20931  rhmsubc  20946  psrplusg  22250  opsrtoslem2  22370  mdetunilem3  22934  mdetunilem4  22935  mdetunilem9  22940  imacmp  23720  ptuncnv  24131  tgphaus  24441  tsmsres  24468  tsmsxplem1  24477  tsmsxplem2  24478  trust  24553  metreslem  24686  imasdsf1olem  24697  xmspropd  24797  mspropd  24798  imasf1oxms  24813  imasf1oms  24814  nmpropd2  24919  isngp2  24921  ngppropd  24961  tngngp2  24976  cphsscph  25577  cmspropd  25675  cmssmscld  25676  mbfres2  25971  limciun  26219  dvmptres3  26281  dvmptres2  26287  dvmptntr  26296  dvlipcn  26319  dvlip2  26320  c1liplem1  26321  dvgt0lem1  26327  lhop1lem  26338  dvcnvrelem1  26342  dvcvx  26345  ftc2ditglem  26370  wilthlem2  27401  dchrval  27566  dchrelbas2  27569  noresle  28059  nosupcbv  28064  nosupno  28065  nosupdm  28066  nosupfv  28068  nosupres  28069  nosupbnd1lem1  28070  nosupbnd1lem3  28072  nosupbnd1lem5  28074  nosupbnd1  28076  nosupbnd2  28078  noinfcbv  28079  noinfno  28080  noinfdm  28081  noinffv  28083  noinfres  28084  noinfbnd1lem3  28087  noinfbnd1lem5  28089  noinfbnd1  28091  noinfbnd2  28093  noetalem1  28103  norecov  28338  norec2ov  28348  egrsubgr  29863  pfxwlk  30271  dfpth2  30319  pthhashvtx  30320  pthdlem1  30357  eupthvdres  30841  eupth2lem3  30842  eupth2  30845  eucrct2eupth  30851  hhssablo  31870  hhssnvt  31872  hhsssh  31876  fresunsn  33266  fressupp  33328  resf1o  33368  gsummpt2d  33656  gsumpart  33670  symgcom  33690  tocycval  33715  tocycfv  33716  tocycf  33724  tocyc01  33725  cycpm2tr  33726  cycpmconjslem1  33761  cycpmconjslem2  33762  nsgqusf1o  34013  extvval  34209  extvfval  34210  extvfvcl  34214  qtophaus  34514  esumcvg  34764  eulerpartlemn  35059  sseqp1  35073  signsvtn0  35245  ftc2re  35273  reprsuc  35290  bnj1385  35508  bnj1326  35702  bnj1321  35703  bnj1442  35725  bnj1450  35726  bnj1463  35731  bnj1529  35746  cvmliftlem5  36140  cvmliftlem7  36142  cvmliftlem10  36145  cvmliftlem11  36146  cvmliftlem15  36149  cvmlift2lem11  36164  cvmlift2lem12  36165  satffunlem1lem1  36253  satffunlem2lem1  36255  eldm3  36618  funsseq  36625  finixpnum  38621  poimirlem3  38634  poimirlem4  38635  poimirlem9  38640  sdclem2  38769  prdsbnd2  38822  isdivrngo  38977  drngoi  38978  elrefsymrels2  39678  eleqvrels2  39701  dibffval  42290  hdmapffval  42976  hdmapfval  42977  eqresfnbd  43379  dvun  43503  eldiophb  43861  diophrw  43863  diophin  43876  tfsconcatrev  44443  ofoafg  44449  resisoeq45d  44514  rclexi  44708  rtrclex  44710  rtrclexi  44714  cnvrcl0  44718  dfrtrcl5  44722  dfrcl2  44767  fvmptiunrelexplb0da  44778  sblpnf  45387  fresin2  46280  limsupresuz  46806  limsupvaluz  46811  limsupvaluz2  46841  supcnvlimsup  46843  climrescn  46851  liminfresuz  46887  cncfuni  46989  dvresntr  47021  dvbdfbdioolem1  47031  itgiccshift  47083  itgperiod  47084  dirkercncflem2  47207  fourierdlem46  47255  fourierdlem48  47257  fourierdlem49  47258  fourierdlem58  47267  fourierdlem72  47281  fourierdlem74  47283  fourierdlem75  47284  fourierdlem81  47290  fourierdlem88  47297  fourierdlem89  47298  fourierdlem90  47299  fourierdlem91  47300  fourierdlem92  47301  fourierdlem103  47312  fourierdlem104  47313  fourierdlem112  47321  fouriersw  47334  voncmpl  47724  tmachlem-agreeself  48039  tmachlem-agreeprod  48040  funcoressn  48205  funressnmo  48209  f1cof1blem  48237  funfocofob  48241  funressndmafv2rn  48386  f1oresf1orab  48452  upgrimpths  49100  isubgrgrim  49120  stgrfv  49144  gpgov  49233  rngcidALTV  49464  rhmsubcALTVlem3  49473  funcringcsetcALTV2lem5  49484  ringcidALTV  49498  funcringcsetclem5ALTV  49507  itcoval  49866  itcoval0mpt  49871  itcovalendof  49874  idfu1sta  50310  idfu2nda  50312  imaidfu2  50320  idfullsubc  50370  dfswapf2  50476  oppc1stf  50503  oppc2ndf  50504  1stfpropd  50505  2ndfpropd  50506  fucofvalg  50533  fucof1  50537  fucofvalne  50540  opf2fval  50633  idfudiag1  50753  aacllem  51107