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 ⊢ (𝜑 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1563   ↾ cres 5654

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-in 3914  df-opab 5168  df-xp 5658  df-res 5664

This theorem is referenced by:  reseq12d  5970  imadifssran  6140  resresdm  6224  relresfld  6267  fnunres1  6637  f1orescnv  6826  fococnv2  6837  fvn0ssdmfun  7059  fnressn  7145  fnsnsplit  7172  oprssov  7569  curry1  8087  curry2  8090  dftpos2  8227  frecseq123  8267  fpr3g  8270  frrlem1  8271  frrlem4  8274  frrlem12  8282  fpr2a  8287  wfr3g  8304  dfrecs3  8347  tfrlem16  8368  tfr2ALT  8376  tfr3ALT  8377  on2recsov  8642  sbthlem4  9066  mapunen  9122  hartogslem1  9492  frr3g  9716  frr2  9720  axdc3lem2  10423  fseq1p1m1  13617  resunimafz0  14472  hashf1lem1  14482  relexp0g  15049  relexp0  15050  relexpsucnnr  15052  dfrtrcl2  15089  bpolylem  16092  setsval  17217  idfuval  17923  idfu2nd  17924  resf1st  17941  idfusubc0  17946  idfusubc  17947  setcid  18133  catcisolem  18157  estrcid  18180  funcestrcsetclem5  18190  funcsetcestrclem5  18205  funcsetcestrclem7  18207  1stfval  18237  1stf2  18239  2ndfval  18240  2ndf2  18242  1stfcl  18243  2ndfcl  18244  curf2ndf  18293  hofcl  18305  isps  18614  cnvps  18624  isdir  18644  dirref  18647  tsrdir  18650  frmdval  18900  frmdplusg  18903  gsum2dlem2  20032  dprd2da  20105  dpjval  20119  ablfac1eulem  20135  ablfac1eu  20136  rngcval  20694  rnghmsubcsetclem1  20707  rngccat  20710  rngcid  20711  rngcifuestrc  20715  funcrngcsetc  20716  funcrngcsetcALT  20717  ringcval  20723  rhmsubcsetclem1  20736  ringccat  20739  ringcid  20740  rhmsubcrngclem1  20742  rhmsubcrngc  20744  funcringcsetc  20750  rhmsubc  20765  psrplusg  22047  opsrtoslem2  22167  mdetunilem3  22732  mdetunilem4  22733  mdetunilem9  22738  imacmp  23515  ptuncnv  23925  tgphaus  24235  tsmsres  24262  tsmsxplem1  24271  tsmsxplem2  24272  trust  24347  metreslem  24480  imasdsf1olem  24491  xmspropd  24591  mspropd  24592  imasf1oxms  24607  imasf1oms  24608  nmpropd2  24713  isngp2  24715  ngppropd  24755  tngngp2  24770  cphsscph  25371  cmspropd  25469  cmssmscld  25470  mbfres2  25765  limciun  26014  dvmptres3  26076  dvmptres2  26082  dvmptntr  26091  dvlipcn  26114  dvlip2  26115  c1liplem1  26116  dvgt0lem1  26122  lhop1lem  26133  dvcnvrelem1  26137  dvcvx  26140  ftc2ditglem  26165  wilthlem2  27191  dchrval  27356  dchrelbas2  27359  noresle  27819  nosupcbv  27824  nosupno  27825  nosupdm  27826  nosupfv  27828  nosupres  27829  nosupbnd1lem1  27830  nosupbnd1lem3  27832  nosupbnd1lem5  27834  nosupbnd1  27836  nosupbnd2  27838  noinfcbv  27839  noinfno  27840  noinfdm  27841  noinffv  27843  noinfres  27844  noinfbnd1lem3  27847  noinfbnd1lem5  27849  noinfbnd1  27851  noinfbnd2  27853  noetalem1  27863  norecov  28098  norec2ov  28108  egrsubgr  29536  dfpth2  29987  pthdlem1  30024  eupthvdres  30495  eupth2lem3  30496  eupth2  30499  eucrct2eupth  30505  hhssablo  31524  hhssnvt  31526  hhsssh  31530  fresunsn  32882  fressupp  32945  resf1o  32987  gsummpt2d  33282  gsumpart  33296  symgcom  33316  tocycval  33341  tocycfv  33342  tocycf  33350  tocyc01  33351  cycpm2tr  33352  cycpmconjslem1  33387  cycpmconjslem2  33388  nsgqusf1o  33641  extvval  33838  extvfval  33839  extvfvcl  33843  qtophaus  34143  esumcvg  34393  eulerpartlemn  34688  sseqp1  34702  signsvtn0  34874  ftc2re  34902  reprsuc  34919  bnj1385  35137  bnj1326  35331  bnj1321  35332  bnj1442  35354  bnj1450  35355  bnj1463  35360  bnj1529  35375  f1resfz0f1d  35476  pfxwlk  35487  pthhashvtx  35491  cvmliftlem5  35652  cvmliftlem7  35654  cvmliftlem10  35657  cvmliftlem11  35658  cvmliftlem15  35661  cvmlift2lem11  35676  cvmlift2lem12  35677  satffunlem1lem1  35765  satffunlem2lem1  35767  eldm3  36124  funsseq  36131  finixpnum  38116  poimirlem3  38134  poimirlem4  38135  poimirlem9  38140  sdclem2  38253  prdsbnd2  38306  isdivrngo  38461  drngoi  38462  elrefsymrels2  39164  eleqvrels2  39187  dibffval  41776  hdmapffval  42462  hdmapfval  42463  eqresfnbd  42863  dvun  42980  eldiophb  43350  diophrw  43352  diophin  43365  tfsconcatrev  43937  ofoafg  43943  resisoeq45d  44008  rclexi  44203  rtrclex  44205  rtrclexi  44209  cnvrcl0  44213  dfrtrcl5  44217  dfrcl2  44262  fvmptiunrelexplb0da  44273  sblpnf  44884  fresin2  45748  limsupresuz  46275  limsupvaluz  46280  limsupvaluz2  46310  supcnvlimsup  46312  climrescn  46320  liminfresuz  46356  cncfuni  46458  dvresntr  46490  dvbdfbdioolem1  46500  itgiccshift  46552  itgperiod  46553  dirkercncflem2  46676  fourierdlem46  46724  fourierdlem48  46726  fourierdlem49  46727  fourierdlem58  46736  fourierdlem72  46750  fourierdlem74  46752  fourierdlem75  46753  fourierdlem81  46759  fourierdlem88  46766  fourierdlem89  46767  fourierdlem90  46768  fourierdlem91  46769  fourierdlem92  46770  fourierdlem103  46781  fourierdlem104  46782  fourierdlem112  46790  fouriersw  46803  voncmpl  47193  funcoressn  47634  funressnmo  47638  f1cof1blem  47666  funfocofob  47670  funressndmafv2rn  47815  f1oresf1orab  47881  upgrimpths  48529  isubgrgrim  48549  stgrfv  48573  gpgov  48662  rngcidALTV  48894  rhmsubcALTVlem3  48903  funcringcsetcALTV2lem5  48914  ringcidALTV  48928  funcringcsetclem5ALTV  48937  itcoval  49292  itcoval0mpt  49297  itcovalendof  49300  idfu1sta  49730  idfu2nda  49732  imaidfu2  49740  idfullsubc  49790  dfswapf2  49890  oppc1stf  49917  oppc2ndf  49918  1stfpropd  49919  2ndfpropd  49920  fucofvalg  49947  fucof1  49951  fucofvalne  49954  opf2fval  50034  idfudiag1  50154  aacllem  50430